equal
deleted
inserted
replaced
231 end; |
231 end; |
232 |
232 |
233 fun register_subclass (sub, sup) some_dep_morph some_wit export thy = |
233 fun register_subclass (sub, sup) some_dep_morph some_wit export thy = |
234 let |
234 let |
235 val intros = (snd o rules thy) sup :: map_filter I |
235 val intros = (snd o rules thy) sup :: map_filter I |
236 [Option.map (Drule.standard' o Element.conclude_witness) some_wit, |
236 [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit, |
237 (fst o rules thy) sub]; |
237 (fst o rules thy) sub]; |
238 val tac = EVERY (map (TRYALL o Tactic.rtac) intros); |
238 val tac = EVERY (map (TRYALL o Tactic.rtac) intros); |
239 val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup)) |
239 val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup)) |
240 (K tac); |
240 (K tac); |
241 val diff_sort = Sign.complete_sort thy [sup] |
241 val diff_sort = Sign.complete_sort thy [sup] |