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 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
12 Local_Theory.note (thm_name, (flat thms)) lthy |> snd |
13 |
13 fun setup_proof (name_spec, (txt, _)) lthy = |
14 fun setup_proof (name_spec, (txt, pos)) lthy = |
|
15 let |
14 let |
16 val trm = ML_Context.evaluate lthy true ("r", r) txt |
15 val trm = ML_Context.evaluate lthy true ("r", r) txt |
17 in |
16 in |
18 Proof.theorem NONE (after_qed name_spec) [[(trm,[])]] lthy |
17 Proof.theorem NONE (after_qed name_spec) [[(trm,[])]] lthy |
19 end |
18 end |
20 |
19 |
21 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
20 val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source |
22 in |
21 in |
23 OuterSyntax.local_theory_to_proof "prove" "proving a proposition" |
22 Outer_Syntax.local_theory_to_proof "prove" "proving a proposition" |
24 OuterKeyword.thy_goal (parser >> setup_proof) |
23 Keyword.thy_goal (parser >> setup_proof) |
25 end |
24 end |
26 *} |
25 *} |
27 |
26 |
28 end |
27 end |