equal
deleted
inserted
replaced
1158 ML%linenosgray{*let |
1158 ML%linenosgray{*let |
1159 fun goal_prop str lthy = |
1159 fun goal_prop str lthy = |
1160 let |
1160 let |
1161 val prop = Syntax.read_prop lthy str |
1161 val prop = Syntax.read_prop lthy str |
1162 in |
1162 in |
1163 Proof.theorem_i NONE (K I) [[(prop,[])]] lthy |
1163 Proof.theorem NONE (K I) [[(prop, [])]] lthy |
1164 end |
1164 end |
1165 |
1165 |
1166 val kind = OuterKeyword.thy_goal |
1166 val kind = OuterKeyword.thy_goal |
1167 in |
1167 in |
1168 OuterSyntax.local_theory_to_proof "foobar_goal" "proves a proposition" |
1168 OuterSyntax.local_theory_to_proof "foobar_goal" "proves a proposition" |
1171 |
1171 |
1172 text {* |
1172 text {* |
1173 The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be |
1173 The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be |
1174 proved) and a context as argument. The context is necessary in order to be able to use |
1174 proved) and a context as argument. The context is necessary in order to be able to use |
1175 @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition. |
1175 @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition. |
1176 In Line 6 the function @{ML_ind theorem_i in Proof} starts the proof for the |
1176 In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the |
1177 proposition. Its argument @{ML NONE} stands for a locale (which we chose to |
1177 proposition. Its argument @{ML NONE} stands for a locale (which we chose to |
1178 omit); the argument @{ML "(K I)"} stands for a function that determines what |
1178 omit); the argument @{ML "(K I)"} stands for a function that determines what |
1179 should be done with the theorem once it is proved (we chose to just forget |
1179 should be done with the theorem once it is proved (we chose to just forget |
1180 about it). Line 9 contains the parser for the proposition. |
1180 about it). Line 9 contains the parser for the proposition. |
1181 |
1181 |
1209 |
1209 |
1210 fun setup_proof (thm_name, (txt, pos)) lthy = |
1210 fun setup_proof (thm_name, (txt, pos)) lthy = |
1211 let |
1211 let |
1212 val trm = ML_Context.evaluate lthy true ("r", r) txt |
1212 val trm = ML_Context.evaluate lthy true ("r", r) txt |
1213 in |
1213 in |
1214 Proof.theorem_i NONE (after_qed thm_name) [[(trm,[])]] lthy |
1214 Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy |
1215 end |
1215 end |
1216 |
1216 |
1217 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
1217 val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source |
1218 in |
1218 in |
1219 OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" |
1219 OuterSyntax.local_theory_to_proof "foobar_prove" "proving a proposition" |