equal
deleted
inserted
replaced
165 val typedef_thms = |
165 val typedef_thms = |
166 [#type_definition (#2 info), #below_def cpo_info, emb_def, prj_def, defl_def, |
166 [#type_definition (#2 info), #below_def cpo_info, emb_def, prj_def, defl_def, |
167 liftemb_def, liftprj_def, liftdefl_def] |
167 liftemb_def, liftprj_def, liftdefl_def] |
168 val thy = lthy |
168 val thy = lthy |
169 |> Class.prove_instantiation_instance |
169 |> Class.prove_instantiation_instance |
170 (K (Tactic.rtac (@{thm typedef_domain_class} OF typedef_thms) 1)) |
170 (K (rtac (@{thm typedef_domain_class} OF typedef_thms) 1)) |
171 |> Local_Theory.exit_global |
171 |> Local_Theory.exit_global |
172 |
172 |
173 (*other theorems*) |
173 (*other theorems*) |
174 val defl_thm' = Thm.transfer thy defl_def |
174 val defl_thm' = Thm.transfer thy defl_def |
175 val (DEFL_thm, thy) = thy |
175 val (DEFL_thm, thy) = thy |