HomeIsabelle/Phabricator

no separate code-equations required for a lift_definition by using (code_dt)…

Description

no separate code-equations required for a lift_definition by using (code_dt) instead

Details