equal
deleted
inserted
replaced
6 val r = ref (NONE:(unit -> term) option) |
6 val r = ref (NONE:(unit -> term) option) |
7 *} |
7 *} |
8 |
8 |
9 ML {* |
9 ML {* |
10 let |
10 let |
11 fun setup_proof (txt, pos) lthy = |
11 fun after_qed thm_name thms lthy = |
12 let |
12 LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd |
13 val trm = ML_Context.evaluate lthy true ("r", r) txt |
13 |
14 in |
14 fun setup_proof (name_spec, (txt, pos)) lthy = |
15 Proof.theorem_i NONE (K I) [[(trm,[])]] lthy |
15 let |
16 end; |
16 val trm = ML_Context.evaluate lthy true ("r", r) txt |
|
17 in |
|
18 Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy |
|
19 end; |
17 |
20 |
18 val setup_proof_parser = OuterParse.ML_source >> setup_proof |
21 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
19 |
22 |
20 val kind = OuterKeyword.thy_goal |
|
21 in |
23 in |
22 OuterSyntax.local_theory_to_proof "prove" "proving a proposition" |
24 OuterSyntax.local_theory_to_proof "prove" "proving a proposition" |
23 kind setup_proof_parser |
25 OuterKeyword.thy_goal (parser >> setup_proof) |
24 end |
26 end |
25 *} |
27 *} |
26 |
28 |
27 |
29 |
28 |
30 |