equal
deleted
inserted
replaced
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 |
18 Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy |
18 Proof.theorem 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 in |
22 in |
23 OuterSyntax.local_theory_to_proof "prove" "proving a proposition" |
23 OuterSyntax.local_theory_to_proof "prove" "proving a proposition" |