equal
deleted
inserted
replaced
1068 |
1068 |
1069 *} |
1069 *} |
1070 |
1070 |
1071 ML_val{*val r = ref (NONE:(unit -> term) option)*} |
1071 ML_val{*val r = ref (NONE:(unit -> term) option)*} |
1072 ML{*let |
1072 ML{*let |
1073 fun setup_proof (txt, pos) lthy = |
1073 fun after_qed thm_name thms lthy = |
|
1074 LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd |
|
1075 |
|
1076 fun setup_proof (thm_name, (txt, pos)) lthy = |
1074 let |
1077 let |
1075 val trm = ML_Context.evaluate lthy true ("r", r) txt |
1078 val trm = ML_Context.evaluate lthy true ("r", r) txt |
1076 in |
1079 in |
1077 Proof.theorem_i NONE (K I) [[(trm,[])]] lthy |
1080 Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy |
1078 end; |
1081 end |
1079 |
1082 |
1080 val setup_proof_parser = OuterParse.ML_source >> setup_proof |
1083 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
1081 |
1084 |
1082 val kind = OuterKeyword.thy_goal |
|
1083 in |
1085 in |
1084 OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
1086 OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
1085 kind setup_proof_parser |
1087 OuterKeyword.thy_goal (parser >> setup_proof) |
1086 end*} |
1088 end*} |
1087 |
1089 |
1088 foobar_prove {* @{prop "True"} *} |
1090 foobar_prove test: {* @{prop "True"} *} |
1089 apply(rule TrueI) |
1091 apply(rule TrueI) |
1090 done |
1092 done |
1091 |
1093 |
1092 (* |
1094 (* |
1093 ML {* |
1095 ML {* |