equal
deleted
inserted
replaced
7 *} |
7 *} |
8 |
8 |
9 ML {* |
9 ML {* |
10 let |
10 let |
11 fun after_qed thm_name thms lthy = |
11 fun after_qed thm_name thms lthy = |
12 LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd |
12 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
13 |
13 |
14 fun setup_proof (name_spec, (txt, pos)) lthy = |
14 fun setup_proof (name_spec, (txt, pos)) lthy = |
15 let |
15 let |
16 val trm = ML_Context.evaluate lthy true ("r", r) txt |
16 val trm = ML_Context.evaluate lthy true ("r", r) txt |
17 in |
17 in |