equal
deleted
inserted
replaced
76 fun prove_assm_intro thm = |
76 fun prove_assm_intro thm = |
77 let |
77 let |
78 val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt; |
78 val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt; |
79 val thm'' = Morphism.thm (const_morph $> eq_morph) thm'; |
79 val thm'' = Morphism.thm (const_morph $> eq_morph) thm'; |
80 val tac = ALLGOALS (ProofContext.fact_tac [thm'']); |
80 val tac = ALLGOALS (ProofContext.fact_tac [thm'']); |
81 in Goal.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end; |
81 in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end; |
82 val assm_intro = Option.map prove_assm_intro |
82 val assm_intro = Option.map prove_assm_intro |
83 (fst (Locale.intros_of thy class)); |
83 (fst (Locale.intros_of thy class)); |
84 |
84 |
85 (* of_class *) |
85 (* of_class *) |
86 val of_class_prop_concl = Logic.mk_inclass (aT, class); |
86 val of_class_prop_concl = Logic.mk_inclass (aT, class); |
93 val base_sort_trivs = Drule.sort_triv thy (aT, base_sort); |
93 val base_sort_trivs = Drule.sort_triv thy (aT, base_sort); |
94 val tac = REPEAT (SOMEGOAL |
94 val tac = REPEAT (SOMEGOAL |
95 (Tactic.match_tac (axclass_intro :: sup_of_classes |
95 (Tactic.match_tac (axclass_intro :: sup_of_classes |
96 @ loc_axiom_intros @ base_sort_trivs) |
96 @ loc_axiom_intros @ base_sort_trivs) |
97 ORELSE' Tactic.assume_tac)); |
97 ORELSE' Tactic.assume_tac)); |
98 val of_class = Goal.prove_global thy [] [] of_class_prop (K tac); |
98 val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac); |
99 |
99 |
100 in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end; |
100 in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end; |
101 |
101 |
102 |
102 |
103 (* reading and processing class specifications *) |
103 (* reading and processing class specifications *) |