equal
deleted
inserted
replaced
134 val liftprj_eqn = |
134 val liftprj_eqn = |
135 Logic.mk_equals (liftprj_const newT, mk_u_map (prj_const newT)) |
135 Logic.mk_equals (liftprj_const newT, mk_u_map (prj_const newT)) |
136 val liftdefl_eqn = |
136 val liftdefl_eqn = |
137 Logic.mk_equals (liftdefl_const newT, |
137 Logic.mk_equals (liftdefl_const newT, |
138 Abs ("t", Term.itselfT newT, |
138 Abs ("t", Term.itselfT newT, |
139 mk_capply (@{const pdefl}, defl_const newT $ Logic.mk_type newT))) |
139 mk_capply (@{const liftdefl_of}, defl_const newT $ Logic.mk_type newT))) |
140 |
140 |
141 val name_def = Binding.suffix_name "_def" name |
141 val name_def = Binding.suffix_name "_def" name |
142 val emb_bind = (Binding.prefix_name "emb_" name_def, []) |
142 val emb_bind = (Binding.prefix_name "emb_" name_def, []) |
143 val prj_bind = (Binding.prefix_name "prj_" name_def, []) |
143 val prj_bind = (Binding.prefix_name "prj_" name_def, []) |
144 val defl_bind = (Binding.prefix_name "defl_" name_def, []) |
144 val defl_bind = (Binding.prefix_name "defl_" name_def, []) |