equal
deleted
inserted
replaced
40 *} |
40 *} |
41 |
41 |
42 ML {* |
42 ML {* |
43 val r = ref (NONE:(unit -> term) option) |
43 val r = ref (NONE:(unit -> term) option) |
44 *} |
44 *} |
45 ML {* |
45 ML{* |
46 let |
46 let |
47 fun setup_proof (txt, pos) lthy = |
47 fun after_qed thm_name thms lthy = |
|
48 LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd |
|
49 |
|
50 fun setup_proof (thm_name, (txt, pos)) lthy = |
48 let |
51 let |
49 val trm = ML_Context.evaluate lthy true ("r", r) txt |
52 val trm = ML_Context.evaluate lthy true ("r", r) txt |
50 in |
53 in |
51 Proof.theorem_i NONE (K I) [[(trm,[])]] lthy |
54 Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy |
52 end; |
55 end |
53 |
56 |
54 val setup_proof_parser = OuterParse.ML_source >> setup_proof |
57 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
55 |
58 |
56 val kind = OuterKeyword.thy_goal |
|
57 in |
59 in |
58 OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
60 OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
59 kind setup_proof_parser |
61 OuterKeyword.thy_goal (parser >> setup_proof) |
60 end |
62 end*} |
61 *} |
63 |
62 |
64 |
63 (* |
65 (* |
64 ML {* |
66 ML {* |
65 let |
67 let |
66 val do_nothing = Scan.succeed (LocalTheory.theory I) |
68 val do_nothing = Scan.succeed (LocalTheory.theory I) |