equal
deleted
inserted
replaced
35 |> maps snd |
35 |> maps snd |
36 |> the_single |
36 |> the_single |
37 |> ObjectLogic.ensure_propT thy; |
37 |> ObjectLogic.ensure_propT thy; |
38 fun after_qed thm = |
38 fun after_qed thm = |
39 LocalTheory.theory (Class.prove_subclass (sub, sup) thm) |
39 LocalTheory.theory (Class.prove_subclass (sub, sup) thm) |
40 #> LocalTheory.reinit; |
40 #> (TheoryTarget.init (SOME sub) o ProofContext.theory_of); |
41 in |
41 in |
42 do_proof after_qed sublocale_prop lthy |
42 do_proof after_qed sublocale_prop lthy |
43 end; |
43 end; |
44 |
44 |
45 fun user_proof after_qed prop = |
45 fun user_proof after_qed prop = |