1.1 --- a/src/Tools/isac/Interpret/script.sml	Wed May 08 18:45:25 2019 +0200
     1.2 +++ b/src/Tools/isac/Interpret/script.sml	Fri May 10 15:59:58 2019 +0200
     1.3 @@ -1090,24 +1090,38 @@
     1.4           (m', (Selem.ScrState scrst, ctxt), (v, Selem.Sundef)))                      (*next stac*)
     1.5    | next_tac _ _ _ (is, _) = error ("next_tac: not impl for " ^ (Selem.istate2str is));
     1.6  
     1.7 -(*.create the initial interpreter state from the items of the guard.*)
     1.8 +(* create the initial interpreter state
     1.9 +  from the items of the guard and the formal arguments of the partial_function.
    1.10 +Note on progression from (a) type fmz_ \<longrightarrow> (e) arguments of the partial_function:
    1.11 +  (a) fmz is given by a math author
    1.12 +  (b) fmz_ is transformed to ori list as a prerequisite for efficient interactive modelling
    1.13 +  (c) modelling creates an itm list from ori list + possible user input
    1.14 +  (d) specifying a theory might add some items and create a guard for the partial_function
    1.15 +  (e) fun relate_args creates an environment for evaluating the partial_function.
    1.16 +Note on sequence-relation (a) -- (e), i.e. the (formal) arguments of the partial_function:
    1.17 +  * Since the arguments of the partial_function have no description (see Descript.thy),
    1.18 +    (e) depends on the sequence in fmz_ and on the types of the formal arguments.
    1.19 +  * pairing formal arguments with itm's follows the sequence
    1.20 +  * Thus the resulting sequence-relation can be ambiguous.
    1.21 +  * Ambiguities are done by rearranging fmz_ or the formal arguments.
    1.22 +  * The latter is easier, albeit not optimal: a fmz_ can be used by different partial_functions.
    1.23 +  *)
    1.24  local
    1.25  val errmsg = "ERROR: found no actual arguments for prog. of "
    1.26 -fun msg_miss (sc, metID, formals, actuals) =
    1.27 -  "ERROR in creating the environment for '" ^ id_of_scr sc ^ 
    1.28 -	"' from \nthe items of the guard of " ^ Celem.metID2str metID ^ ",\n" ^
    1.29 -	"formal arg(s), from the script, miss actual arg(s), from the guards LTool.env:\n" ^
    1.30 -	(string_of_int o length) formals ^ " formals: " ^ Rule.terms2str formals ^ "\n" ^
    1.31 -	(string_of_int o length) actuals ^ " actuals: " ^ Rule.terms2str actuals
    1.32 -fun msg_type (sc, metID, a, f, formals, actuals) =
    1.33 -  "ERROR in creating the environment for '" ^
    1.34 -	id_of_scr sc ^ "' from \nthe items of the guard of " ^
    1.35 -	Celem.metID2str metID ^ ",\n" ^
    1.36 -	"different types of formal arg, from the script, " ^
    1.37 -	"and actual arg, from the guards LTool.env:'\n" ^
    1.38 -	"formal: '" ^ Rule.term2str a ^ "::" ^ (Rule.type2str o type_of) a ^ "'\n" ^
    1.39 -	"actual: '" ^ Rule.term2str f ^ "::" ^ (Rule.type2str o type_of) f ^ "'\n" ^
    1.40 -	"in\n" ^
    1.41 +fun msg_miss sc metID caller f formals actuals =
    1.42 +  "ERROR in creating the environment from formal args. of partial_function \"" ^ id_of_scr sc ^ "\"\n" ^
    1.43 +	"and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
    1.44 +	"formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
    1.45 +	"with:\n" ^
    1.46 +	(string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
    1.47 +	(string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
    1.48 +fun msg_ambiguous sc metID f aas formals actuals =
    1.49 +  "ERROR in creating the environment from formal args. of partial_function \"" ^ id_of_scr sc ^ "\"\n" ^
    1.50 +	"and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
    1.51 +  "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..."  ^
    1.52 +  "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
    1.53 +  "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^
    1.54 +	"with\n" ^
    1.55  	"formals: " ^ Rule.terms2str formals ^ "\n" ^
    1.56  	"actuals: " ^ Rule.terms2str actuals
    1.57  in
    1.58 @@ -1118,14 +1132,19 @@
    1.59      val (scr, sc) = (case (#scr o Specify.get_met) metID of
    1.60         scr as Rule.Prog sc => (scr, sc) | _ => raise ERROR ("init_scrstate with " ^ Celem.metID2str metID))
    1.61      val formals = formal_args sc    
    1.62 -	  (*expects same sequence of (actual) args in itms and (formal) args in met*)
    1.63 -	  fun relate_args env [] [] = env
    1.64 -	    | relate_args _ _ [] = error (msg_miss (sc, metID, formals, actuals))
    1.65 -	    | relate_args env [] _ = env (*may drop Find!*)
    1.66 -	    | relate_args env (a::aa) (f::ff) = 
    1.67 -	      if type_of a = type_of f 
    1.68 -	      then relate_args (env @ [(a, f)]) aa ff
    1.69 -        else error (msg_type (sc, metID, a, f, formals, actuals))
    1.70 +    fun assoc_by_type f aa =
    1.71 +      case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
    1.72 +        [] => error (msg_miss sc metID "assoc_by_type" f formals actuals)
    1.73 +      | [a] => (f, a)
    1.74 +      | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
    1.75 +	  fun relate_args _ (f::_)  [] = error (msg_miss sc metID "relate_args" f formals actuals)
    1.76 +	    | relate_args env [] _ = env (*may drop Find?*)
    1.77 +	    | relate_args env (f::ff) (aas as (a::aa)) = 
    1.78 +	      if type_of f = type_of a 
    1.79 +	      then relate_args (env @ [(f, a)]) ff aa
    1.80 +        else
    1.81 +          let val (f, a) = assoc_by_type f aas
    1.82 +          in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
    1.83      val env = relate_args [] formals actuals;
    1.84      val ctxt = Proof_Context.init_global thy |> Stool.declare_constraints' actuals
    1.85      val {pre, prls, ...} = Specify.get_met metID;

     2.1 --- a/src/Tools/isac/Interpret/specification-elems.sml	Wed May 08 18:45:25 2019 +0200
     2.2 +++ b/src/Tools/isac/Interpret/specification-elems.sml	Fri May 10 15:59:58 2019 +0200
     2.3 @@ -55,8 +55,8 @@
     2.4  struct
     2.5  
     2.6  type fmz_ = Rule.cterm' list;
     2.7 -(* a formalization of an example containing data 
     2.8 -   sufficient for mechanically finding the solution for the example
     2.9 +(* a formalization of an example contains data 
    2.10 +   sufficient for mechanically finding the solution for the example.
    2.11     FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)
    2.12  type fmz = fmz_ * Celem.spec;
    2.13  val e_fmz = ([], Celem.e_spec);

     3.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy	Wed May 08 18:45:25 2019 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy	Fri May 10 15:59:58 2019 +0200
     3.3 @@ -31,11 +31,12 @@
     3.4    FunktionsVariable        :: "real => una"
     3.5    Funktionen               :: "bool list => una"
     3.6    Gleichungen              :: "bool list => una"
     3.7 +  GleichungsVariablen      :: "real list => una"
     3.8  
     3.9    (*Script-names*)
    3.10 -  Biegelinie2Script        :: "[real,real,real,real=>real,bool list,
    3.11 +  Biegelinie2Script        :: "[real, real, real, real => real, bool list, real list,
    3.12  				bool] => bool"	
    3.13 -	("((Script Biegelinie2Script (_ _ _ _ _ =))// (_))" 9)
    3.14 +	("((Script Biegelinie2Script (_ _ _ _ _ _=))// (_))" 9)
    3.15    BiegelinieScript         :: "[real,real,real,real=>real,bool list,bool list,
    3.16  				bool] => bool"	
    3.17  	("((Script BiegelinieScript (_ _ _ _ _ _ =))// (_))" 9)
    3.18 @@ -212,7 +213,8 @@
    3.19  setup \<open>KEStore_Elems.add_mets
    3.20      [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
    3.21  	    (["IntegrierenUndKonstanteBestimmen2"],
    3.22 -	      [("#Given" ,["Traegerlaenge l", "Streckenlast q", "FunktionsVariable v"]),
    3.23 +	      [("#Given" ,["Traegerlaenge l", "Streckenlast q",
    3.24 +              "FunktionsVariable v", "GleichungsVariablen vs"]),
    3.25  		      (*("#Where",["0 < l"]), ...wait for &lt; and handling Arbfix*)
    3.26  		      ("#Find"  ,["Biegelinie b"]),
    3.27  		      ("#Relate",["Randbedingungen s"])],
    3.28 @@ -230,7 +232,7 @@
    3.29  				        Rule.Thm ("if_False",TermC.num_str @{thm if_False})],
    3.30  				  prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},
    3.31          "Script Biegelinie2Script                                                                           " ^
    3.32 -        "(l::real) (q :: real) (v :: real) (b :: real => real) (s :: bool list) =                           " ^
    3.33 +        "(l::real) (q :: real) (v :: real) (b :: real => real) (s :: bool list) (vs :: real list) =                           " ^
    3.34          "  (let                                                                                             " ^
    3.35          "    (funs :: bool list) = (SubProblem (''Biegelinie'',                                                " ^
    3.36          "      [''vonBelastungZu'', ''Biegelinien''], [''Biegelinien'', ''ausBelastung''])                                  " ^
    3.37 @@ -240,7 +242,7 @@
    3.38          "      [BOOL_LIST funs, BOOL_LIST s]);                                                              " ^
    3.39          "    (cons :: bool list) = (SubProblem (''Biegelinie'',                                                " ^
    3.40          "      [''LINEAR'', ''system''], [''no_met''])                                                                  " ^
    3.41 -        "      [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]);                                             " ^
    3.42 +        "      [BOOL_LIST equs, REAL_LIST vs]);                                             " ^
    3.43          "    B = Take (lastI funs);                                                                         " ^
    3.44          "    B = ((Substitute cons) @@                                                                      " ^
    3.45          "           (Rewrite_Set_Inst [(''bdv'', v)] ''make_ratpoly_in'' False)) B                                  " ^

     4.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed May 08 18:45:25 2019 +0200
     4.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Fri May 10 15:59:58 2019 +0200
     4.3 @@ -94,7 +94,7 @@
     4.4        fun_arg = Take (lhs X');                                                      
     4.5        arg = (Rewrite_Set ''partial_fraction'' False) X';                     \<comment> \<open>get_argument TODO\<close>      
     4.6        L_L = SubProblem (''Test'', [''LINEAR'',''univariate'',''equation'',''test''],         
     4.7 -                [''Test'',''solve_linear'']) [BOOL equ, REAL z]              \<comment> \<open>PROG --> as arg\<close>
     4.8 +                [''Test'',''solve_linear'']) [BOOL equ, REAL z]
     4.9    in X) "
    4.10  *)
    4.11  setup \<open>KEStore_Elems.add_mets

     5.1 --- a/test/Tools/isac/Frontend/states.sml	Wed May 08 18:45:25 2019 +0200
     5.2 +++ b/test/Tools/isac/Frontend/states.sml	Fri May 10 15:59:58 2019 +0200
     5.3 @@ -17,7 +17,7 @@
     5.4  let (*wraps whole test*)
     5.5  val ex = [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
     5.6      "Randbedingungen [Q 0 = q_0 * L, M_b L = 0, y 0 = 0, y' 0 = 0]",
     5.7 -    "FunktionsVariable x"],
     5.8 +    "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]"],
     5.9    ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
    5.10  
    5.11  fun real_of_time t = (Time.toMicroseconds t |> real) / 1000.0

     6.1 --- a/test/Tools/isac/Interpret/script.sml	Wed May 08 18:45:25 2019 +0200
     6.2 +++ b/test/Tools/isac/Interpret/script.sml	Fri May 10 15:59:58 2019 +0200
     6.3 @@ -18,6 +18,7 @@
     6.4  "----------- fun dsc_valT ----------------------------------------";
     6.5  "----------- fun itms2args ---------------------------------------";
     6.6  "----------- fun rep_tac_ ----------------------------------------";
     6.7 +"----------- fun init_scrstate -----------------------------------------------------------------";
     6.8  "-----------------------------------------------------------------";
     6.9  "-----------------------------------------------------------------";
    6.10  "-----------------------------------------------------------------";
    6.11 @@ -586,3 +587,36 @@
    6.12  > val (lhs,_)=tac_2etac m';
    6.13  > lhs'=lhs;
    6.14  val it = true : bool*)
    6.15 +
    6.16 +"----------- fun init_scrstate -----------------------------------------------------------------";
    6.17 +"----------- fun init_scrstate -----------------------------------------------------------------";
    6.18 +"----------- fun init_scrstate -----------------------------------------------------------------";
    6.19 +val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
    6.20 +	     "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
    6.21 +	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]"];
    6.22 +val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
    6.23 +		     ["IntegrierenUndKonstanteBestimmen2"]);
    6.24 +val p = e_pos'; val c = [];
    6.25 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
    6.26 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
    6.27 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
    6.28 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
    6.29 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
    6.30 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
    6.31 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
    6.32 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
    6.33 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
    6.34 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
    6.35 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
    6.36 +(*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt''''' = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
    6.37 +
    6.38 +val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');
    6.39 +"~~~~~ fun init_scrstate , args:"; val (thy, itms, metID) = (assoc_thy thy, meth, metID);
    6.40 +val (ScrState st, ctxt, Prog _) = init_scrstate thy itms metID;
    6.41 +if scrstate2str st =
    6.42 +"([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, y)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\"], [], NONE, \n??.empty, Safe, true)"
    6.43 +then () else error "init_scrstate changed for Biegelinie";
    6.44 +
    6.45 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)
    6.46 +if p = ([1], Pbl) andalso (fst nxt) = "Model_Problem" then ()
    6.47 +else error "modeling root-problem of Biegelinie 7.70 changed";

     7.1 --- a/test/Tools/isac/Knowledge/biegelinie-2.sml	Wed May 08 18:45:25 2019 +0200
     7.2 +++ b/test/Tools/isac/Knowledge/biegelinie-2.sml	Fri May 10 15:59:58 2019 +0200
     7.3 @@ -128,7 +128,7 @@
     7.4  "----- Bsp 7.70 with me";
     7.5  val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
     7.6  	     "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]",
     7.7 -	     "FunktionsVariable x"];
     7.8 +	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]"];
     7.9  val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
    7.10  		     ["IntegrierenUndKonstanteBestimmen2"]);
    7.11  val p = e_pos'; val c = [];

     8.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Wed May 08 18:45:25 2019 +0200
     8.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Fri May 10 15:59:58 2019 +0200
     8.3 @@ -844,7 +844,7 @@
     8.4  reset_states ();
     8.5  CalcTree [(["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
     8.6  	     "Randbedingungen [M_b L = 0, y 0 = 0, y L = 0, y' 0 = 0]",
     8.7 -	     "FunktionsVariable x"],
     8.8 +	     "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]"],
     8.9  	    ("Biegelinie", ["Biegelinien"],
    8.10  	     ["IntegrierenUndKonstanteBestimmen2"] ))];
    8.11  moveActiveRoot 1;
    8.12 @@ -878,7 +878,7 @@
    8.13  reset_states ();
    8.14  CalcTree [(["Traegerlaenge L","Streckenlast (q_0 / L * x)","Biegelinie y",
    8.15  	    "Randbedingungen [M_b 0 = 0, M_b L = 0, y 0 = 0, y L = 0]",
    8.16 -	    "FunktionsVariable x"],
    8.17 +	    "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]"],
    8.18  	   ("Biegelinie", ["Biegelinien"],
    8.19  	    ["IntegrierenUndKonstanteBestimmen2"] ))];
    8.20  moveActiveRoot 1;

     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/test/Tools/isac/Test_Some_meld.thy	Fri May 10 15:59:58 2019 +0200
     9.3 @@ -0,0 +1,95 @@
     9.4 +theory Test_Some_meld imports Isac.Build_Thydata
     9.5 +begin 
     9.6 +ML \<open>
     9.7 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     9.8 +                      (* these vvv test, if funs are intermediately opened in structure 
     9.9 +                         in case of errors here consider ~~/./xtest-to-coding.sh      *)
    9.10 +  open Kernel;
    9.11 +  open Math_Engine;            CalcTreeTEST;
    9.12 +  open Lucin;                  appy;
    9.13 +  open Inform;                 cas_input;
    9.14 +  open Rtools;                 trtas2str;
    9.15 +  open Chead;                  pt_extract;
    9.16 +  open Generate;               (* NONE *)
    9.17 +  open Ctree;                  append_problem;
    9.18 +  open Specify;                show_ptyps;
    9.19 +  open Applicable;             mk_set;
    9.20 +  open Solve;                  (* NONE *)
    9.21 +  open Selem;                  e_fmz;
    9.22 +  open Stool;                  transfer_asms_from_to;
    9.23 +  open Tac;                    (* NONE *)
    9.24 +  open Model;                  (* NONE *)
    9.25 +  open LTool;                  rule2stac;
    9.26 +  open Rewrite;                mk_thm;
    9.27 +  open Calc;                   get_pair;
    9.28 +  open TermC;                  atomt;
    9.29 +  open Celem;                  e_pbt;
    9.30 +  open Rule;                   string_of_thm;
    9.31 +  open Tools;                  eval_lhs;
    9.32 +(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    9.33 +\<close>
    9.34 +ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
    9.35 +
    9.36 +section \<open>code for copy & paste ===============================================================\<close>
    9.37 +ML \<open>
    9.38 +"~~~~~ fun xxx , args:"; val () = ();
    9.39 +"~~~~~ and xxx , args:"; val () = ();                                                                                     
    9.40 +
    9.41 +"~~~~~ to xxx return val:"; val () = ();
    9.42 +
    9.43 +\<close>
    9.44 +text \<open>
    9.45 +  declare [[show_types]] 
    9.46 +  declare [[show_sorts]]            
    9.47 +  find_theorems "?a <= ?a"
    9.48 +  
    9.49 +  print_theorems
    9.50 +  print_facts
    9.51 +  print_statement ""
    9.52 +  print_theory
    9.53 +  ML_command \<open>Pretty.writeln prt\<close>
    9.54 +  declare [[ML_print_depth = 999]]
    9.55 +  declare [[ML_exception_trace]]
    9.56 +\<close>
    9.57 +ML \<open>
    9.58 +(*========== inhibit exn WN130909 TODO =========================================================
    9.59 +============ inhibit exn WN130909 TODO ========================================================*)
    9.60 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    9.61 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
    9.62 +\<close>
    9.63 +
    9.64 +section \<open>===================================================================================\<close>
    9.65 +ML \<open>
    9.66 +"~~~~~ fun xxx, args:"; val () = ();
    9.67 +\<close> ML \<open>
    9.68 +\<close> ML \<open>
    9.69 +\<close> ML \<open>
    9.70 +"~~~~~ fun xxx, args:"; val () = ();
    9.71 +\<close>
    9.72 +
    9.73 +section \<open>===================================================================================\<close>
    9.74 +ML \<open>
    9.75 +"~~~~~ fun xxx , args:"; val () = ();
    9.76 +\<close> ML \<open>
    9.77 +\<close> ML \<open>
    9.78 +\<close> ML \<open>
    9.79 +"~~~~~ fun xxx , args:"; val () = ();
    9.80 +\<close>
    9.81 +
    9.82 +section \<open>===================================================================================\<close>
    9.83 +ML \<open>
    9.84 +"~~~~~ fun xxx , args:"; val () = ();
    9.85 +\<close> ML \<open>
    9.86 +\<close> ML \<open>
    9.87 +\<close> ML \<open>
    9.88 +"~~~~~ fun xxx , args:"; val () = ();
    9.89 +\<close>
    9.90 +
    9.91 +section \<open>code for copy & paste ===============================================================\<close>
    9.92 +ML \<open>
    9.93 +"~~~~~ fun xxx , args:"; val () = ();
    9.94 +"~~~~~ and xxx , args:"; val () = ();
    9.95 +
    9.96 +"~~~~~ to xxx  return val:"; val () = ();
    9.97 +\<close>
    9.98 +end