equal
deleted
inserted
replaced
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 |
18 Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy |
18 Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy |
19 end; |
19 end |
20 |
20 |
21 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
21 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
22 |
|
23 in |
22 in |
24 OuterSyntax.local_theory_to_proof "prove" "proving a proposition" |
23 OuterSyntax.local_theory_to_proof "prove" "proving a proposition" |
25 OuterKeyword.thy_goal (parser >> setup_proof) |
24 OuterKeyword.thy_goal (parser >> setup_proof) |
26 end |
25 end |
27 *} |
26 *} |
28 |
27 |
29 |
|
30 |
|
31 end |
28 end |