equal
deleted
inserted
replaced
73 val morph = base_morph $> eq_morph; |
73 val morph = base_morph $> eq_morph; |
74 |
74 |
75 (* assm_intro *) |
75 (* assm_intro *) |
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 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 SkipProof.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)); |