1.1 --- a/test/Pure/Isar/Test_Parsers_Cookbook.thy Sat Jul 18 16:38:58 2020 +0200
1.2 +++ b/test/Pure/Isar/Test_Parsers_Cookbook.thy Mon Jul 20 12:19:59 2020 +0200
1.3 @@ -225,17 +225,12 @@
1.4 \<close> ML \<open>
1.5 \<close>
1.6
1.7 -subsection \<open>Problem_headline\<close>
1.8 +subsection \<open>problem_headline\<close>
1.9 ML \<open>
1.10 -val toks = filtered_input (
1.11 - (**)
1.12 - "Problem" ^ (**)
1.13 - "(" (**) ^
1.14 - "\"Biegelinie\"" (**) ^
1.15 - "," (**) ^
1.16 - " [\"Biegelinien\"]" (**) ^
1.17 - ")" (**)
1.18 -)
1.19 +\<close> ML \<open>
1.20 +val problem_headline_str = "Problem ( \"Biegelinie\" , [\"Biegelinien\"] )"
1.21 +\<close> ML \<open>
1.22 +val toks = filtered_input problem_headline_str
1.23 \<close> ML \<open>
1.24 parse (Parse.$$$ "Problem") toks
1.25 \<close> ML \<open>
1.26 @@ -270,17 +265,29 @@
1.27 subsubsection \<open>Model\<close>
1.28 ML \<open>
1.29 \<close> ML \<open>
1.30 -val toks = filtered_input (
1.31 +val toks1 = filtered_input (
1.32 " Model:" ^
1.33 " Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
1.34 " Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
1.35 " Find: \"Biegelinie y\"" ^
1.36 " Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\""
1.37 )
1.38 -(* = [Token (("Model", ({}, {})), (Keyword, "Model"), Slot)]*)
1.39 +\<close> ML \<open>
1.40 +val toks2 = filtered_input (
1.41 +" Model ( RProblem ) :" ^
1.42 + (*^^^^^^^^^^^*)
1.43 +" Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
1.44 +" Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
1.45 +" Find: \"Biegelinie y\"" ^
1.46 +" Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\""
1.47 +)
1.48 \<close> ML \<open>
1.49 val model = (
1.50 - Parse.$$$ "Model" -- Parse.$$$ ":" --
1.51 + Parse.$$$ "Model" --
1.52 + (Scan.optional
1.53 + (Parse.$$$ "(" -- (Parse.$$$ "RProblem" || Parse.$$$ "RMethod") -- Parse.$$$ ")")
1.54 + (("", ""), "")) --
1.55 + Parse.$$$ ":" --
1.56 Parse.$$$ "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term --
1.57 Parse.$$$ "Where" -- Parse.$$$ ":" -- Parse.list Parse.term --
1.58 Parse.$$$ "Find" -- Parse.$$$ ":" -- Parse.term --
1.59 @@ -289,15 +296,25 @@
1.60 \<close> ML \<open>
1.61 val model' = Scan.finite Token.stopper model
1.62 \<close> ML \<open>
1.63 -model' toks
1.64 +model' toks1
1.65 (* =
1.66 - (((((((((((((("Model", ":"),
1.67 + ((((((((((((((
1.68 + "Model", ":"), (* <--------------------------------------------*)
1.69 "Given"), ":"), ["<markup>", "<markup>"]),
1.70 "Where"), ":"), ["<markup>", "<markup>"]),
1.71 "Find"), ":"), "<markup>"),
1.72 "Relate"), ":"), ["<markup>"]),
1.73 [])*)
1.74 \<close> ML \<open>
1.75 +model' toks2
1.76 +(* =
1.77 + (((((((((((((((
1.78 + "Model", (("(", "RProblem"), ")")), ":"), (* <--------------------------------------------*)
1.79 + "Given"), ":"), ["<markup>", "<markup>"]),
1.80 + "Where"), ":"), ["<markup>", "<markup>"]),
1.81 + "Find"), ":"), "<markup>"),
1.82 + "Relate"), ":"), ["<markup>"]), [])*)
1.83 +\<close> ML \<open>
1.84 \<close>
1.85
1.86 subsubsection \<open>References\<close>
1.87 @@ -371,9 +388,10 @@
1.88
1.89 subsubsection \<open>Specification: Model -- References\<close>
1.90 ML \<open>
1.91 -val toks = filtered_input (
1.92 +\<close> ML \<open>
1.93 +val specification_str = (
1.94 " Specification:" ^
1.95 -" Model:"^
1.96 +" Model:" ^
1.97 " Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
1.98 " Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^
1.99 " Find: \"Biegelinie y\"" ^
1.100 @@ -384,6 +402,8 @@
1.101 " RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]" (**)
1.102 )
1.103 \<close> ML \<open>
1.104 +val toks = filtered_input specification_str
1.105 +\<close> ML \<open>
1.106 length toks = 37;
1.107 \<close> ML \<open>
1.108 val specification_whole = (
1.109 @@ -414,21 +434,19 @@
1.110 subsubsection \<open>Specification: Scan.optional Model -- References\<close>
1.111 ML \<open>
1.112 \<close> ML \<open>
1.113 - (model -- references)
1.114 -:
1.115 -((((((((((((((string * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
1.116 - ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list)) parser
1.117 + (model -- references):
1.118 +(((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
1.119 + ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list)) parser
1.120 \<close> ML \<open>
1.121 -type model_refs = ((((((((((((((string * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
1.122 +type model_refs = (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
1.123 ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))
1.124 \<close> ML \<open>
1.125 val string = "";
1.126 -val e_model_refs = (((((((((((((("", ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []),
1.127 +val e_model_refs = ((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []),
1.128 (((((((((("", ""), ""), ""), ""), ""), ""), []), ""), ""), []))
1.129 \<close> ML \<open>
1.130 e_model_refs : model_refs
1.131 \<close> ML \<open>
1.132 -
1.133 \<close> ML \<open>
1.134 val specification = (
1.135 (Parse.$$$ "Specification" -- Parse.$$$ ":") (**) --
1.136 @@ -437,24 +455,28 @@
1.137 ) (**)
1.138 e_model_refs
1.139 )
1.140 -\<close> ML \<open>
1.141 -specification toks (*..whole Specification from above -----------------------------------------*)
1.142 +\<close> ML \<open> (*whole Specification from above -----------------------------------------------------\*)
1.143 +specification toks
1.144 \<close> ML \<open>
1.145 case specification toks of (((
1.146 "Specification", ":"),
1.147 - ((((((((((((((
1.148 - "Model", ":"), "Given"), ":"), [_, _]), "Where"), ":"), [_, _]), "Find"), ":"), _), "Relate"), ":"), [_]),
1.149 + (((((((((((((((
1.150 + "Model", (("", ""), "")), ":"),
1.151 + "Given"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
1.152 + "Where"), ":"), [_(*"<markup>"*), _(*"<markup>"*)]),
1.153 + "Find"), ":"), _(*"<markup>"*)),
1.154 + "Relate"), ":"), [_(*"<markup>"*)]),
1.155 ((((((((((
1.156 "References", ":"),
1.157 "RTheory"), ":"), "Biegelinie"),
1.158 "RProblem"), ":"), ["Biegelinien"]),
1.159 "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"]))),
1.160 - ([] : Token.T list)) => () | _ => error "parse specification (expanded) changed"
1.161 + ([] : Token.T list)) => () | _ => error "parse specification (expanded) changed"
1.162 \<close> ML \<open>
1.163 (specification toks) : ((string * string) * model_refs) * Token.T list
1.164 \<close> ML \<open>
1.165 -\<close> ML \<open>
1.166 -val toks = filtered_input ( (*.. Specification collapsed --------------------------------------*)
1.167 +\<close> ML \<open> (*Specification collapsed ------------------------------------------------------------\*)
1.168 +val toks = filtered_input (
1.169 " Specification:" (** ) ^
1.170 " Model:"^
1.171 " Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^
1.172 @@ -467,16 +489,13 @@
1.173 " RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]" ( **)
1.174 )
1.175 \<close> ML \<open>
1.176 -val (((
1.177 - "Specification", ":"),
1.178 - (((((((((((((("", ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (*model*)
1.179 - (((((((((("", ""), ""), ""), ""), ""), ""), []), ""), ""), []))), []) = (*refs*)
1.180 - parse specification toks
1.181 +\<close> ML \<open>
1.182 +parse specification toks
1.183 \<close> ML \<open>
1.184 case parse specification toks of (((
1.185 "Specification", ":"),
1.186 - (((((((((((((("", ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (*model*)
1.187 - (((((((((("", ""), ""), ""), ""), ""), ""), []), ""), ""), []))), []) (*refs*)
1.188 +(*model*)((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []),
1.189 +(*refs*)(((((((((("", ""), ""), ""), ""), ""), ""), []), ""), ""), []))), [])
1.190 => () | _ => error "parse specification (collapsed) changed"
1.191
1.192 \<close> ML \<open>
1.193 @@ -487,28 +506,132 @@
1.194 Problem is recursively possible in Solution.
1.195 for recursive parsers see p.140 \<section>6.2: parse_tree
1.196 \<close>
1.197 +subsubsection \<open>tactics\<close>
1.198 +ML \<open>
1.199 +val toks1 = filtered_input "Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\""
1.200 +val substitute = Parse.reserved "Substitute" -- Parse.term -- Parse.term;
1.201 +case substitute toks1 of ((("Substitute", _(*<markup>*)), _(*<markup>*)), [])
1.202 +=> () | _ => error "parse Substitute CHANGED";
1.203 +\<close> ML \<open>
1.204 +val toks2 = filtered_input "Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\""
1.205 +val rewrite_set_inst = Parse.reserved "Rewrite_Set_Inst" -- Parse.term -- Parse.name;
1.206 +case rewrite_set_inst toks2 of
1.207 + ((("Rewrite_Set_Inst", _(*<markup>*)), "make_ratpoly_in"), [])
1.208 +=> () | _ => error "parse Rewrite_Set_Inst CHANGED";
1.209 +\<close> ML \<open>
1.210 +val toks3 = filtered_input "Check_Postcond [\"Biegelinien\", \"xxx\"]"
1.211 +val check_postcond = Parse.reserved "Check_Postcond" --
1.212 + (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]");
1.213 +case check_postcond toks3 of (("Check_Postcond", ["Biegelinien", "xxx"]), [])
1.214 +=> () | _ => error "parse Check_Postcond CHANGED"
1.215 +\<close> ML \<open>
1.216 +\<close> ML \<open>
1.217 +\<close> ML \<open> (* see test/../Test_Parsers.thy \<open>|| requires arguments of equal type; 2 tricks that help:\<close>
1.218 + semantics is NOT YET fully understood *)
1.219 +fun exec_substitute ((str, tm), bdv) =
1.220 + "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*UnparseC.term*) tm ^ " " ^ (*UnparseC.term*) bdv;
1.221 +fun exec_rewrite_set_inst ((str, tm), id) =
1.222 + "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*UnparseC.term*) tm ^ " " ^ (*Problem.id_to_string*) id;
1.223 +fun exec_check_postcond (str, path) =
1.224 + "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*Problem.id_to_string*)fold (curry op ^) path "";
1.225 +\<close> ML \<open>
1.226 +\<close> ML \<open>
1.227 +val toks1' = filtered_input "Tactic Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\""
1.228 +val toks2' = filtered_input "Tactic Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\""
1.229 +val toks3' = filtered_input "Tactic Check_Postcond [\"Biegelinien\", \"xxx\"]"
1.230 +\<close> ML \<open>
1.231 +val tactic = ( (* incomplete list of tactics *)
1.232 +Parse.$$$ "Tactic" --
1.233 + (substitute >> exec_substitute (**) ||
1.234 + rewrite_set_inst >> exec_rewrite_set_inst (**)||
1.235 + check_postcond >> exec_check_postcond (**)
1.236 + )
1.237 +)
1.238 +\<close> ML \<open>
1.239 +parse tactic toks1'; (* = (("Tactic", "EXEC IMMEDIATELY: Substitute <markup> <markup>"), [])*)
1.240 +parse tactic toks2'; (* = (("Tactic", "EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"), [])*)
1.241 +parse tactic toks3'; (* = (("Tactic", "EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien"), [])*)
1.242 +\<close> ML \<open>
1.243 +\<close>
1.244 +
1.245 +subsubsection \<open>steps\<close>
1.246 ML \<open>
1.247 \<close> ML \<open>
1.248 -val toks = filtered_input ( (*Problem.. postponed, some term shortened*)
1.249 +val toks1 = filtered_input
1.250 + "\"[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\""
1.251 +val toks2 = filtered_input (
1.252 + "\"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\"" ^
1.253 + " Tactic Check_Postcond [\"Biegelinien\"]")
1.254 +\<close> ML \<open>
1.255 +val toks3 = filtered_input (
1.256 +" \"[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\"" (**) ^
1.257 +" \"y x = c_4 + c_3 * x + 1 / (-1 * EI)\"" (**) ^
1.258 +" Tactic Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\"" (**) ^
1.259 +" \"y x = 0 + 0 * x + 1 / (-1 * EI)\"" (**) ^
1.260 +" Tactic Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\"" (**) ^
1.261 +" \"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\"" (**) ^
1.262 +" Tactic Check_Postcond [\"Biegelinien\"]" (**) ^
1.263 +" \"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\"" (**)
1.264 +)
1.265 +\<close> ML \<open>
1.266 +val steps = (Scan.repeat (Parse.term -- (Scan.optional tactic ("", ""))))
1.267 +:
1.268 +(string * (string * string)) list parser
1.269 +\<close> ML \<open>
1.270 +parse steps []; (* = ([], []): (string * (string * string)) list * Token.T list *)
1.271 +parse steps toks1; (* = ([("<markup>", ("", ""))], [])*)
1.272 +parse steps toks2; (* = ([("<markup>", ("Tactic", "EXEC IMMEDIATELY: Check_Postcond Biegelinien"))], [])*)
1.273 +\<close> ML \<open>
1.274 +parse steps toks3;
1.275 +\<close> ML \<open>
1.276 +case parse steps toks3 of
1.277 + ([(_(*"<markup>"*), ("", "")),
1.278 + (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Substitute <markup> <markup>"*))),
1.279 + (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"*))),
1.280 + (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Check_Postcond Biegelinien"*))),
1.281 + (_(*"<markup>"*), ("", ""))],
1.282 + [])
1.283 +=> () | _ => error "parse steps CHANGED";
1.284 +\<close> ML \<open>
1.285 +\<close>
1.286 +
1.287 +subsubsection \<open>solution\<close>
1.288 +ML \<open>
1.289 +\<close> ML \<open>
1.290 +val solution_str = ( (*Problem.. postponed, some term shortened*)
1.291 " Solution:" (**) ^
1.292 (* HOW HANDLE THIS SPECIFIC Problem ?..
1.293 - "solveSystem [L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3] [c, c_1, c_2, c_4]"*)
1.294 -" [c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]" (**) ^
1.295 -" y x = c_4 + c_3 * x + 1 / (-1 * EI)" (**) ^
1.296 + "solveSystem \"[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3]\" \"[c, c_1, c_2, c_4]\""*)
1.297 +" \"[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\"" (**) ^
1.298 +" \"y x = c_4 + c_3 * x + 1 / (-1 * EI)\"" (**) ^
1.299 " Tactic Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\"" (**) ^
1.300 -" y x = 0 + 0 * x + 1 / (-1 * EI)" (**) ^
1.301 -" Tactic Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\" \"y x\"" (**) ^
1.302 -" y x = -6 * q_0 * L ^ 2 / (-24 * EI)" (**) ^
1.303 -" Tactic Check_Postcond [\"Biegelinien\"]" (**)
1.304 +" \"y x = 0 + 0 * x + 1 / (-1 * EI)\"" (**) ^
1.305 +" Tactic Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\"" (**) ^
1.306 +" \"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\"" (**) ^
1.307 +" Tactic Check_Postcond [\"Biegelinien\"]" (**) ^
1.308 +" \"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\"" (**)
1.309 )
1.310 \<close> ML \<open>
1.311 +val toks = filtered_input solution_str
1.312 +\<close> ML \<open>
1.313 +val solution = Parse.$$$ "Solution" -- Parse.$$$ ":" -- steps
1.314 +\<close> ML \<open>
1.315 +parse solution toks
1.316 +\<close> ML \<open>
1.317 +case parse solution toks of
1.318 + ((("Solution", ":"),
1.319 + [(_(*"<markup>"*), ("", "")),
1.320 + (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Substitute <markup> <markup>"*))),
1.321 + (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Rewrite_Set_Inst <markup> make_ratpoly_in"*))),
1.322 + (_(*"<markup>"*), ("Tactic", _(*"EXEC IMMEDIATELY: Check_Postcond Biegelinien"*))),
1.323 + (_(*"<markup>"*), ("", ""))]),
1.324 + [])
1.325 +=> () | _ => error "parse solution CHANGED";
1.326 +\<close> ML \<open>
1.327 \<close>
1.328
1.329 subsection \<open>Problem: headline + Specification + Solution\<close>
1.330 -subsubsection \<open>TOWARDS Specification + Solution general\<close>
1.331 -text \<open>
1.332 - COMPARE subsubsection \<open>Cookbook Scan.optional p.146 \<section>6.7\<close> IN THIS FILE
1.333 -\<close>
1.334 +subsubsection \<open>TOWARDS Specification + Solution general: Scan.optional ?!?\<close>
1.335 ML \<open>
1.336 \<close> ML \<open>
1.337 val toks = filtered_input (
1.338 @@ -572,15 +695,34 @@
1.339 \<close> ML \<open>
1.340 \<close>
1.341
1.342 -subsubsection \<open>Specification + Solution collapsed\<close>
1.343 +subsubsection \<open>whole Problem\<close>
1.344 +ML \<open>
1.345 +\<close> ML \<open>
1.346 +val toks = filtered_input (problem_headline_str ^ specification_str ^ solution_str)
1.347 +\<close> ML \<open>
1.348 +val problem = problem_headline -- specification -- solution
1.349 +\<close> ML \<open>
1.350 +val problem' = Scan.finite Token.stopper problem
1.351 +\<close> ML \<open>
1.352 +case problem' toks of (_, []) => () | _ => error "parse whole Problem CHANGED 1"
1.353 +\<close> ML \<open>
1.354 +\<close>
1.355 +
1.356 +subsubsection \<open>Problem collapsed in variants\<close>
1.357 text \<open>
1.358 - The variants of input below should be accepted by the final calc_parser
1.359 + The variants of input below should be accepted by the final calc_parser "problem'.
1.360 + An occasion to improve parsers' error messages !"
1.361 \<close>
1.362 ML \<open>
1.363 \<close> ML \<open>
1.364 -val toks = filtered_input (
1.365 -" Problem ( \"Biegelinie\" , [\"Biegelinien\"] )"
1.366 -)
1.367 +val toks = filtered_input problem_headline_str
1.368 +\<close> text \<open>
1.369 +problem' toks
1.370 +(*ERROR exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
1.371 +\<close> ML \<open>
1.372 +problem_headline_str
1.373 +\<close> ML \<open>
1.374 +\<close> ML \<open>
1.375 \<close> ML \<open>
1.376 val toks = filtered_input (
1.377 " Problem ( \"Biegelinie\" , [\"Biegelinien\"] )" (**) ^
1.378 @@ -598,4 +740,13 @@
1.379 \<close> ML \<open>
1.380 \<close>
1.381
1.382 -(** )end( * Missing outer syntax command(s) "ISAC" *)
1.383 +subsubsection \<open>Problem - Solution recursively\<close>
1.384 +ML \<open>
1.385 +\<close> ML \<open>
1.386 +\<close> ML \<open>
1.387 +\<close> ML \<open>
1.388 +\<close> ML \<open>
1.389 +\<close> ML \<open>
1.390 +\<close>
1.391 +
1.392 +(**)end (* Missing outer syntax command(s) "ISAC" *)