1.1 --- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Thu Oct 08 10:05:33 2020 +0200
1.2 +++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Thu Oct 22 14:03:40 2020 +0200
1.3 @@ -12,7 +12,7 @@
1.4
1.5 spark_open \<open>greatest_common_divisor/g_c_d\<close>
1.6
1.7 -spark_vc procedure_g_c_d_4
1.8 +spark_vc procedure_g_c_d_4 (*..def.in greatest_common_divisor/g_c_d.siv *)
1.9 proof -
1.10 from \<open>0 < d\<close> have "0 \<le> c mod d" by (rule pos_mod_sign)
1.11 with \<open>0 \<le> c\<close> \<open>0 < d\<close> \<open>c - c sdiv d * d \<noteq> 0\<close> show ?C1
2.1 --- a/src/Pure/General/change_table.ML Thu Oct 08 10:05:33 2020 +0200
2.2 +++ b/src/Pure/General/change_table.ML Thu Oct 22 14:03:40 2020 +0200
2.3 @@ -107,6 +107,7 @@
2.4 let
2.5 val Change_Table {change = change1, table = table1} = arg1;
2.6 val Change_Table {change = change2, table = table2} = arg2;
2.7 +(* val _ = writeln ("### join"); WN not found by theorem *)
2.8 in
2.9 if pointer_eq (change1, change2) andalso pointer_eq (table1, table2) then arg1
2.10 else if is_empty arg2 then arg1
3.1 --- a/src/Tools/isac/BridgeJEdit/parseC.sml Thu Oct 08 10:05:33 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml Thu Oct 22 14:03:40 2020 +0200
3.3 @@ -14,7 +14,7 @@
3.4 val tokenize: string -> Token.T list
3.5 val string_of_toks: Token.T list -> string
3.6 val parse: (Token.T list -> 'a * Token.T list) -> Token.T list -> 'a * Token.T list
3.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
3.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
3.9
3.10 (*Problem headline*)
3.11 type problem_headline
3.12 @@ -50,7 +50,7 @@
3.13 val body: body parser
3.14 val body_dummy: body
3.15 val exec_step_term: string * (string * string) -> string
3.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
3.18 end
3.19
3.20 (**)
4.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Thu Oct 08 10:05:33 2020 +0200
4.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Thu Oct 22 14:03:40 2020 +0200
4.3 @@ -230,6 +230,7 @@
4.4 in SOME (thmId, HOLogic.Trueprop $ (TermC.mk_equality (t, t'))) end
4.5 | eval_var _ _ _ _ = NONE;
4.6
4.7 +(* refer to Thm.lhs_of *)
4.8 fun lhs (Const ("HOL.eq",_) $ l $ _) = l
4.9 | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
4.10 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
5.1 --- a/src/Tools/isac/TODO.thy Thu Oct 08 10:05:33 2020 +0200
5.2 +++ b/src/Tools/isac/TODO.thy Thu Oct 22 14:03:40 2020 +0200
5.3 @@ -28,6 +28,8 @@
5.4 \begin{itemize}
5.5 \item xxx
5.6 \item xxx
5.7 + \item relate Prog_Epxr.lhs to Thm.lhs_of
5.8 + \item xxx
5.9 \item as soon as src/../parseC.sml is stable,
5.10 remove defs from Test_Parse_Isac.thy
5.11 + and shift tests from Test_Parse_Isac -> test/../parseC.sml
6.1 --- a/test/Pure/Isar/Check_Outer_Syntax.thy Thu Oct 08 10:05:33 2020 +0200
6.2 +++ b/test/Pure/Isar/Check_Outer_Syntax.thy Thu Oct 22 14:03:40 2020 +0200
6.3 @@ -4,6 +4,7 @@
6.4 (** )"ISAC" :: diag and ( *imported by Test_Parse_Isac*)
6.5 "forthel" :: thy_decl and (*Naproche*)
6.6 "spark_status" :: diag and (*HOL/SPARK*)
6.7 + "spark_vc" :: thy_goal and (*HOL/SPARK*)
6.8 "spark_open_vcg" :: thy_load (*HOL/SPARK*)
6.9 begin
6.10
6.11 @@ -23,7 +24,7 @@
6.12 * ?
6.13 * \<open>Outer_Syntax.command..spark_vc :: thy_goal\<close>
6.14 uses Isabelle's standard proof machinery,
6.15 - so goes directly into inner syntax
6.16 + so goes directly into ???
6.17 * ?
6.18 * \<open>Outer_Syntax.command..spark_open_vcg :: thy_load\<close>
6.19 opens a "SPARK environment",
6.20 @@ -283,6 +284,48 @@
6.21 \<close> ML \<open>
6.22 \<close>
6.23
6.24 +subsection \<open>Outer_Syntax.command..spark_vc :: thy_goal\<close>
6.25 +ML \<open>
6.26 +\<close> ML \<open> (*===== dummy cp.from SPARK/Tools/spark_commands.ML *)
6.27 +\<close> ML \<open>
6.28 +fun lookup_vc (_: theory) (_: bool) (_: string) =
6.29 + (NONE : (Element.context_i list *
6.30 + (string * thm list option * Element.context_i * Element.statement_i)) option)
6.31 +\<close> ML \<open>
6.32 +fun get_vc thy vc_name =
6.33 + (case (*SPARK_VCs.*)lookup_vc thy false vc_name of
6.34 + SOME (ctxt, (_, proved, ctxt', stmt)) =>
6.35 + if is_some proved then
6.36 + error ("The verification condition " ^
6.37 + quote vc_name ^ " has already been proved.")
6.38 + else (ctxt @ [ctxt'], stmt)
6.39 + | NONE => error ("There is no verification condition " ^
6.40 + quote vc_name ^ "."));
6.41 +\<close> ML \<open>
6.42 +fun mark_proved (_: string) (_: thm list) (_: theory) = @{theory Pure}
6.43 +\<close> ML \<open>
6.44 +fun prove_vc vc_name lthy =
6.45 + let
6.46 + val thy = Proof_Context.theory_of lthy;
6.47 + val (ctxt, stmt) = get_vc thy vc_name
6.48 + in(* see text --vvvvvvv*)
6.49 + Specification.theorem true Thm.theoremK NONE
6.50 + (fn thmss => (Local_Theory.background_theory
6.51 + ((*SPARK_VCs.*)mark_proved vc_name (flat thmss))))
6.52 + (Binding.name vc_name, []) [] ctxt stmt false lthy
6.53 + end;
6.54 +\<close> ML \<open>
6.55 +prove_vc: string -> Proof.context -> Proof.state;
6.56 +\<close> ML \<open>
6.57 +(*/---------------------------------------------------------------\*)
6.58 +val _ =
6.59 + Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>spark_vc\<close>
6.60 + "enter into proof mode for a specific verification condition"
6.61 + (Parse.name >> prove_vc);
6.62 +(*\---------------------------------------------------------------/*)
6.63 +\<close> ML \<open>
6.64 +\<close>
6.65 +
6.66 subsection \<open>Outer_Syntax.command..spark_open_vcg :: thy_load\<close>
6.67 ML \<open>
6.68 \<close> ML \<open> (*===== dummy cp.from SPARK/Tools/spark_commands.ML for Outer_Syntax.command..spark_open_vcg*)
6.69 @@ -294,9 +337,10 @@
6.70 \<close> ML \<open>
6.71 \<close> ML \<open> (*===== dummy cp.from SPARK/Tools/fdl_lexer.ML for Outer_Syntax.command..spark_open_vcg*)
6.72 fun vcg_header (_: (string * Position.T) list) =
6.73 - ((("", "", ""), NONE: ((string * string * string) * (string * string * string * string option)) option), []: (string * Position.T) list)
6.74 + ((("", "", ""), NONE: ((string * string * string) * (string * string * string * string option)) option), []: (string * Position.T) list)
6.75 \<close> ML \<open>
6.76 -vcg_header: (string * Position.T) list -> ((string * string * string) * ((string * string * string) * (string * string * string * string option)) option) * (string * Position.T) list
6.77 +vcg_header: (string * Position.T) list ->
6.78 + ((string * string * string) * ((string * string * string) * (string * string * string * string option)) option) * (string * Position.T) list
6.79 \<close> ML \<open>
6.80 val _ =
6.81 Outer_Syntax.command \<^command_keyword>\<open>spark_open_vcg\<close>
6.82 @@ -316,7 +360,13 @@
6.83 val xxx = Resources.provide_parse_files "spark_open_vcg" -- Parse.parname
6.84 : ((theory -> Token.file list * theory) * string) parser;
6.85 xxx: Token.T list -> ((theory -> Token.file list * theory) * string) * Token.T list;
6.86 -(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
6.87 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
6.88 +\<close> ML \<open>
6.89 +Resources.provide_parse_files "spark_open_vcg":
6.90 + (theory -> Token.file list * theory) parser;
6.91 +(* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
6.92 +Parse.parname: ( string) parser;
6.93 +(* ( * ^^^^^^^ *)
6.94 \<close> ML \<open>
6.95 op >>
6.96 (* /------------- 1st arg ---------\ *)
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/test/Pure/Isar/Downto_Synchronized.thy Thu Oct 22 14:03:40 2020 +0200
7.3 @@ -0,0 +1,205 @@
7.4 +chapter \<open>Trace Outer_Syntax.command down to storing proofs\<close>
7.5 +
7.6 +theory Downto_Synchronized
7.7 + imports Pure
7.8 +begin
7.9 +text \<open>
7.10 + We assume, that proofs are stored in a Synchronized.*.
7.11 + We want to re-use as much of Isabelle's proof machinery.
7.12 +\<close>
7.13 +
7.14 +section \<open>Tools for tracing\<close>
7.15 +ML \<open>(*implementation.pdf p.15: output like a record..*)
7.16 +val x = 42;
7.17 +val y = true;
7.18 +\<close> ML \<open>
7.19 +writeln (@{make_string} {x = x, y = y}); (*
7.20 +{x = 42, y = true}
7.21 +val it = (): unit*)
7.22 +\<close> ML \<open>
7.23 +@{print} {x = x, y = y}; (* 1st line normal Output:
7.24 +{x = 42, y = true}\<^here>
7.25 +val it = {x = 42, y = true}: {x: int, y: bool}*)
7.26 +\<close> ML \<open>
7.27 +@{print\<open>tracing\<close>} {x = x, y = y}; (* 1st line blue as tracing:
7.28 +{x = 42, y = true}\<^here>
7.29 +val it = {x = 42, y = true}: {x: int, y: bool}*)
7.30 +\<close>
7.31 +
7.32 +section \<open>Trace code down to Table for..\<close>
7.33 +subsection \<open>Outer_Syntax.command..spark_vc :: thy_goal\<close>
7.34 +text \<open>
7.35 + spark_vc starts an interactive proof, given data for initialising the proof.
7.36 + conclusions:
7.37 + * spark_vc <--> ISAC: Example \<open>exp_Statics_Biegel_Timischl_7-70\<close>
7.38 + * for how to open the data-file \<open>exp_Statics_Biegel_Timischl_7-70\<close> see spark_open
7.39 +\<close> ML \<open>
7.40 +\<close> ML \<open>
7.41 +signature SPECIFICATION =
7.42 +sig
7.43 + val theorem: bool -> string -> Method.text option ->
7.44 + (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
7.45 + string list -> Element.context_i list -> Element.statement_i ->
7.46 + bool -> local_theory -> Proof.state
7.47 +end
7.48 +(** )structure Specification: SPECIFICATION =
7.49 +struct( **)
7.50 +fun gen_theorem (_: bool)
7.51 +(*Bundle.includes:*)
7.52 + (_: string list -> Proof.context -> Proof.context)
7.53 +(*(K I):*)
7.54 + (_: 'a -> 'b -> 'b)
7.55 +(*Expression.cert_statement:*)
7.56 + (_: (Element.context_i list ->
7.57 + Element.statement_i ->
7.58 + Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context)
7.59 + = ()
7.60 +\<close> ML \<open>
7.61 +\<close> ML \<open>
7.62 +val Proof_state = Proof.init @{context}
7.63 +\<close> ML \<open>
7.64 +fun gen_theorem (_: bool) (_:string list) (_:Proof.context) (_:Proof.context) = @{context}
7.65 +\<close> ML \<open>
7.66 +val theorem = (*<----- orig*)
7.67 + gen_theorem false Bundle.includes (K I) Expression.cert_statement;
7.68 +end
7.69 +\<close> ML \<open> (*----- investigate args of theorem..*)
7.70 +Bundle.includes: string list -> Proof.context -> Proof.context
7.71 +\<close> ML \<open>
7.72 +(K I)(*: _b -> _a -> _a*)
7.73 +\<close> ML \<open>
7.74 +Expression.cert_statement: Element.context_i list -> Element.statement_i -> Proof.context ->
7.75 + (Attrib.binding * (term * term list) list) list * Proof.context
7.76 +\<close> ML \<open>
7.77 +\<close> ML \<open> (*----- get type of gen_theorem..*)
7.78 +fun theorem gen_theorem =
7.79 + gen_theorem false Bundle.includes (K I) Expression.cert_statement;
7.80 +\<close> ML \<open>
7.81 +theorem:
7.82 + (bool ->
7.83 +(*Bundle.includes:*)
7.84 + (string list -> Proof.context -> Proof.context) ->
7.85 +(*(K I):*)
7.86 + ('a -> 'b -> 'b) ->
7.87 +(*Expression.cert_statement:*)
7.88 + (Element.context_i list -> Element.statement_i -> Proof.context ->
7.89 + (Attrib.binding * (term * term list) list) list * Proof.context)
7.90 + -> 'c)
7.91 + -> 'c
7.92 +\<close> ML \<open> (*----- replace 'c by Proof.state found in signature SPECIFICATION*)
7.93 +theorem:
7.94 + (bool ->
7.95 +(*Bundle.includes:*)
7.96 + (string list -> Proof.context -> Proof.context) ->
7.97 +(*(K I):*)
7.98 + ('a -> 'b -> 'b) ->
7.99 +(*Expression.cert_statement:*)
7.100 + (Element.context_i list -> Element.statement_i -> Proof.context ->
7.101 + (Attrib.binding * (term * term list) list) list * Proof.context)
7.102 + -> Proof.state)
7.103 + -> Proof.state
7.104 +\<close> ML \<open>
7.105 +
7.106 +
7.107 +signature EXPRESSION =
7.108 +sig
7.109 + val cert_statement: Element.context_i list -> Element.statement_i ->
7.110 + Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
7.111 + val read_statement: Element.context list -> Element.statement ->
7.112 + Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context
7.113 +end
7.114 +structure Expression : EXPRESSION =
7.115 +struct
7.116 +fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;
7.117 +fun read_statement x = prep_statement read_full_context_statement Element.activate x;
7.118 +end
7.119 +
7.120 +
7.121 +signature ELEMENT =
7.122 +sig
7.123 + val activate_i: context_i -> Proof.context -> context_i * Proof.context
7.124 + val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
7.125 +end
7.126 +structure Element: ELEMENT =
7.127 +struct
7.128 +fun activate_i elem ctxt =
7.129 + let
7.130 + val elem' =
7.131 + (case (map_ctxt_attrib o map) Token.init_assignable elem of
7.132 + Defines defs =>
7.133 + Defines (defs |> map (fn ((a, atts), (t, ps)) =>
7.134 + ((Thm.def_binding_optional
7.135 + (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt (K []) t)))) a, atts),
7.136 + (t, ps))))
7.137 + | e => e);
7.138 + val ctxt' = Context.proof_map (init elem') ctxt;
7.139 + in ((map_ctxt_attrib o map) Token.closure elem', ctxt') end;
7.140 +end
7.141 +
7.142 +
7.143 +signature PRIVATE_CONTEXT =
7.144 +sig
7.145 + val proof_map: (generic -> generic) -> Proof.context -> Proof.context
7.146 +end
7.147 +structure Context: PRIVATE_CONTEXT =
7.148 +struct
7.149 +fun proof_map f = the_proof o f o Proof;
7.150 +datatype generic = Theory of theory | Proof of Proof.context;
7.151 +
7.152 +(*/--------------------? related ?-------------------------------------------\*)
7.153 +fun declare_theory_data pos empty extend merge =
7.154 + let
7.155 + val k = serial ();
7.156 + val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
7.157 + val _ = Synchronized.change kinds (Datatab.update (k, kind));
7.158 + in k end; (*^^^^^^^^^^^^^^*)
7.159 +
7.160 +val extend_data = Datatab.map invoke_extend;
7.161 +fun merge_data thys = Datatab.join (invoke_merge thys) o apply2 extend_data;
7.162 + (*^^^^^^^^^^^^^^*)
7.163 +(*private copy avoids potential conflict of table exceptions*)
7.164 +structure Datatab = Table(type key = int val ord = int_ord);
7.165 + (*^^^^*)
7.166 +end
7.167 +
7.168 +signature CHANGE_TABLE =
7.169 +sig
7.170 + structure Table: TABLE
7.171 +end
7.172 +signature TABLE =
7.173 +sig
7.174 + val update: key * 'a -> 'a table -> 'a table
7.175 + val join: (key -> 'a * 'a -> 'a) (*exception SAME*) ->
7.176 + 'a table * 'a table -> 'a table (*exception DUP*)
7.177 +end
7.178 +
7.179 +fun update (key, x) tab = modify key (fn _ => x) tab;
7.180 +(* simultaneous modifications *)
7.181 +fun join f (table1, table2) =
7.182 + let
7.183 + fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
7.184 + in
7.185 + if pointer_eq (table1, table2) then table1
7.186 + else if is_empty table1 then table2
7.187 + else fold_table add table2 table1
7.188 + end;
7.189 +
7.190 +(*============================================================================================
7.191 +search " = Synchronized.var" leads back to Context:
7.192 +
7.193 +val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Any.T) Datatab.table);
7.194 +*)
7.195 +\<close> ML \<open>
7.196 +\<close> ML \<open>
7.197 +\<close>
7.198 +
7.199 +subsection \<open>lemma (from Pure.thy)\<close>
7.200 +theorem meta_mp:
7.201 + assumes "PROP P \<Longrightarrow> PROP Q" and "PROP P"
7.202 + shows "PROP Q"
7.203 + by (rule \<open>PROP P \<Longrightarrow> PROP Q\<close> [OF \<open>PROP P\<close>])
7.204 +
7.205 +
7.206 +
7.207 +
7.208 +end
7.209 \ No newline at end of file
8.1 --- a/test/Pure/Isar/README Thu Oct 08 10:05:33 2020 +0200
8.2 +++ b/test/Pure/Isar/README Thu Oct 22 14:03:40 2020 +0200
8.3 @@ -6,6 +6,7 @@
8.4 Check_Outer_Syntax.thy Survey on checked examples
8.5 Decompose examples: ISAC :: diag, forthel :: thy_decl, spark_status :: diag
8.6 Outer_Syntax.command..spark_open_vcg :: thy_load
8.7 +Downto_Synchorinzed.thy trace code down to storage of a proof
8.8 Keyword_ISAC.thy original from Makarius 2018
8.9 Test_Parse_Isac.thy definitions for keywords
8.10 ^^^^^^^^^^^^^^^^^^^| Tools and Goals
9.1 --- a/test/Pure/Isar/Test_Parse_Isac.thy Thu Oct 08 10:05:33 2020 +0200
9.2 +++ b/test/Pure/Isar/Test_Parse_Isac.thy Thu Oct 22 14:03:40 2020 +0200
9.3 @@ -1109,4 +1109,14 @@
9.4 \<close> ML \<open>
9.5 \<close>
9.6
9.7 +chapter \<open>command_keyword ISAC, avoid error at end\<close>
9.8 +ML \<open> (*original Outer_Syntax.command with trials to adapt with problem parser*)
9.9 +val _ =
9.10 + Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language"
9.11 + (
9.12 + (Parse.input ((**)Parse.cartouche (** )-- (** ) ParseC.( **)problem ( **)))
9.13 + >> (* try variants ^^^^^^^^^^^^^^^ ^^ ^^^^^^^*)
9.14 + (fn input => Toplevel.keep (fn _ => ignore (ML_Lex.read_source input)))
9.15 + )
9.16 +\<close>
9.17 end
9.18 \ No newline at end of file
10.1 --- a/test/Pure/Isar/Theory_Commands.thy Thu Oct 08 10:05:33 2020 +0200
10.2 +++ b/test/Pure/Isar/Theory_Commands.thy Thu Oct 22 14:03:40 2020 +0200
10.3 @@ -1,7 +1,7 @@
10.4 theory Theory_Commands
10.5 imports Main (** )"~~/src/Tools/isac/BridgeJEdit/Isac"( *other Outer_Syntax.command*)
10.6 keywords
10.7 - "ISAC" :: diag and
10.8 + "ISAC" :: thy_decl and
10.9 "Problem" "Specification" "Model" "References" "Solution"
10.10 "Given" "Find" "Relate" "Where"
10.11 "RTheory" "RProblem" "RMethod"
10.12 @@ -61,21 +61,34 @@
10.13
10.14 subsection \<open>command_keyword ISAC\<close>
10.15 ML \<open> (*active*)
10.16 -\<close> ML \<open>
10.17 +\<close> text \<open> (*for "ISAC" :: diag, Outer_Syntax.command*)
10.18 fun check_problem (_: ParseC.problem) =
10.19 fn (_: Toplevel.transition) => Toplevel.empty
10.20 -\<close> ML \<open>
10.21 +
10.22 val _ =
10.23 - Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language"
10.24 + Outer_Syntax.command @ {command_keyword ISAC} "embedded ISAC language"
10.25 (
10.26 ParseC.problem
10.27 >>
10.28 (fn input => Toplevel.keep (fn _ => ignore (check_problem input)))
10.29 )
10.30 -\<close> ML \<open>
10.31 +
10.32 ParseC.problem: ParseC.problem parser;
10.33 check_problem: ParseC.problem -> Toplevel.transition -> Toplevel.transition;
10.34 \<close> ML \<open>
10.35 +\<close> ML \<open> (*for "ISAC" :: thy_decl, Outer_Syntax.local_theory, vvv--- TODO*)
10.36 +fun check_problem (_: Proof.context) (_: ParseC.problem(*, _: Position.T*)) = ();
10.37 +\<close> ML \<open>
10.38 +val _ =
10.39 + Outer_Syntax.local_theory @{command_keyword ISAC} "embedded ISAC language"
10.40 + (
10.41 + ParseC.problem
10.42 + >> (*from naproche.ML..*)
10.43 + (fn inp => fn lthy => (check_problem lthy inp; lthy))
10.44 + )
10.45 +\<close> ML \<open>
10.46 +\<close> ML \<open>
10.47 +\<close> ML \<open>
10.48 \<close>
10.49
10.50 section \<open>Check code with Isac example\<close>