equal
deleted
inserted
replaced
27 let |
27 let |
28 fun prove_prop str lthy = |
28 fun prove_prop str lthy = |
29 let |
29 let |
30 val prop = Syntax.read_prop lthy str |
30 val prop = Syntax.read_prop lthy str |
31 in |
31 in |
32 Proof.theorem_i NONE (K I) [[(prop,[])]] lthy |
32 Proof.theorem NONE (K I) [[(prop,[])]] lthy |
33 end; |
33 end; |
34 val prove_prop_parser = OuterParse.prop >> prove_prop |
34 val prove_prop_parser = OuterParse.prop >> prove_prop |
35 val kind = OuterKeyword.thy_goal |
35 val kind = OuterKeyword.thy_goal |
36 in |
36 in |
37 OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition" |
37 OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition" |
49 |
49 |
50 fun setup_proof (thm_name, (txt, pos)) lthy = |
50 fun setup_proof (thm_name, (txt, pos)) lthy = |
51 let |
51 let |
52 val trm = ML_Context.evaluate lthy true ("r", r) txt |
52 val trm = ML_Context.evaluate lthy true ("r", r) txt |
53 in |
53 in |
54 Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy |
54 Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy |
55 end |
55 end |
56 |
56 |
57 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
57 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
58 |
58 |
59 in |
59 in |