1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Nov 21 17:31:20 2013 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Nov 21 18:12:17 2013 +0100
1.3 @@ -1084,7 +1084,7 @@
1.4 " (equ::bool) = (denom = (0::real)); "^
1.5 " (L_L::bool list) = "^
1.6 " (SubProblem (Test', "^
1.7 - " [linear,univariate,equation,test], "^
1.8 + " [LINEAR,univariate,equation,test], "^
1.9 " [Test,solve_linear]) "^
1.10 " [BOOL equ, REAL z]) "^
1.11 " in X)";
2.1 --- a/test/Tools/isac/Frontend/use-cases.sml Thu Nov 21 17:31:20 2013 +0100
2.2 +++ b/test/Tools/isac/Frontend/use-cases.sml Thu Nov 21 18:12:17 2013 +0100
2.3 @@ -95,7 +95,7 @@
2.4 CalcTree (*start of calculation, return No.1*)
2.5 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.6 ("Test",
2.7 - ["linear","univariate","equation","test"],
2.8 + ["LINEAR","univariate","equation","test"],
2.9 ["Test","solve_linear"]))];
2.10 Iterator 1; (*create an active Iterator on CalcTree No.1*)
2.11
2.12 @@ -127,7 +127,7 @@
2.13 *-----since Model_Problem + complete_mod_ in case cas of SOME-----*)
2.14
2.15 fetchProposedTactic 1;
2.16 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
2.17 + setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
2.18 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.19 (*-------------------------------------------------------------------------*)
2.20 fetchProposedTactic 1;
2.21 @@ -163,7 +163,7 @@
2.22 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.23
2.24 fetchProposedTactic 1;
2.25 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
2.26 + setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
2.27 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.28
2.29 val ((pt,_),_) = get_calc 1;
2.30 @@ -254,7 +254,7 @@
2.31
2.32 fetchProposedTactic 1;(*----------------Subproblem--------------------*);
2.33 setNextTactic 1 (Subproblem ("Test",
2.34 - ["linear","univariate","equation","test"]));
2.35 + ["LINEAR","univariate","equation","test"]));
2.36 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.37
2.38 fetchProposedTactic 1;
2.39 @@ -278,7 +278,7 @@
2.40 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.41
2.42 fetchProposedTactic 1;
2.43 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation","test"]);
2.44 + setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation","test"]);
2.45 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.46 "2-----------------------------------------------------------------";
2.47
2.48 @@ -299,7 +299,7 @@
2.49 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.50
2.51 fetchProposedTactic 1;
2.52 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
2.53 + setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
2.54 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);
2.55
2.56 fetchProposedTactic 1;
2.57 @@ -380,7 +380,7 @@
2.58 CalcTree
2.59 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.60 ("Test",
2.61 - ["linear","univariate","equation","test"],
2.62 + ["LINEAR","univariate","equation","test"],
2.63 ["Test","solve_linear"]))];
2.64 Iterator 1;
2.65 moveActiveRoot 1;
2.66 @@ -404,7 +404,7 @@
2.67 CalcTree
2.68 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.69 ("Test",
2.70 - ["linear","univariate","equation","test"],
2.71 + ["LINEAR","univariate","equation","test"],
2.72 ["Test","solve_linear"]))];
2.73 Iterator 1;
2.74 moveActiveRoot 1;
2.75 @@ -474,16 +474,16 @@
2.76 CalcTree
2.77 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.78 ("Test",
2.79 - ["linear","univariate","equation","test"],
2.80 + ["LINEAR","univariate","equation","test"],
2.81 ["Test","solve_linear"]))];
2.82 Iterator 1;
2.83 moveActiveRoot 1;
2.84 autoCalculate 1 CompleteModel;
2.85 refFormula 1 (get_pos 1 1);
2.86
2.87 -setProblem 1 ["linear","univariate","equation","test"];
2.88 +setProblem 1 ["LINEAR","univariate","equation","test"];
2.89 val pos = get_pos 1 1;
2.90 -setContext 1 pos (kestoreID2guh Pbl_["linear","univariate","equation","test"]);
2.91 +setContext 1 pos (kestoreID2guh Pbl_["LINEAR","univariate","equation","test"]);
2.92 refFormula 1 (get_pos 1 1);
2.93
2.94 setMethod 1 ["Test","solve_linear"];
2.95 @@ -491,7 +491,7 @@
2.96 refFormula 1 (get_pos 1 1);
2.97 val ((pt,_),_) = get_calc 1;
2.98 if get_obj g_spec pt [] = ("e_domID",
2.99 - ["linear", "univariate","equation","test"],
2.100 + ["LINEAR", "univariate","equation","test"],
2.101 ["Test","solve_linear"]) then ()
2.102 else error "FE-interface.sml: diff.behav. in setProblem, setMethod";
2.103
2.104 @@ -628,7 +628,7 @@
2.105 autoCalculate 1 (Step 1); fetchProposedTactic 1;
2.106 setNextTactic 1 (Specify_Theory "PolyEq");
2.107 (*------------- some trials in the problem-hierarchy ---------------*)
2.108 - setNextTactic 1 (Specify_Problem ["linear","univariate","equation"]);
2.109 + setNextTactic 1 (Specify_Problem ["LINEAR","univariate","equation"]);
2.110 autoCalculate 1 (Step 1); fetchProposedTactic 1; (*<ERROR> helpless </ERROR> !!!*)
2.111 setNextTactic 1 (Refine_Problem ["univariate","equation"]);
2.112 (*------------------------------------------------------------------*)
2.113 @@ -708,11 +708,11 @@
2.114 "--------- this is a matching model (all items correct): -------";
2.115 checkContext 1 ([],Pbl) (kestoreID2guh Pbl_ ["univariate","equation"]);
2.116 "--------- this is a NOT matching model (some 'false': ---------";
2.117 -checkContext 1 ([],Pbl)(kestoreID2guh Pbl_ ["linear","univariate","equation"]);
2.118 +checkContext 1 ([],Pbl)(kestoreID2guh Pbl_ ["LINEAR","univariate","equation"]);
2.119
2.120 "--------- find out a matching problem: ------------------------";
2.121 "--------- find out a matching problem (FAILING: no new pbl) ---";
2.122 - refineProblem 1([],Pbl)(pblID2guh ["linear","univariate","equation"]);
2.123 + refineProblem 1([],Pbl)(pblID2guh ["LINEAR","univariate","equation"]);
2.124
2.125 "--------- find out a matching problem (SUCCESSFUL) ------------";
2.126 refineProblem 1 ([],Pbl) (pblID2guh ["univariate","equation"]);
2.127 @@ -928,7 +928,7 @@
2.128 "--------- solve_linear from pbl-hierarchy --------------";
2.129 "--------- solve_linear from pbl-hierarchy --------------";
2.130 "--------- solve_linear from pbl-hierarchy --------------";
2.131 - val (fmz, sp) = ([], ("", ["linear","univariate","equation","test"], []));
2.132 + val (fmz, sp) = ([], ("", ["LINEAR","univariate","equation","test"], []));
2.133 CalcTree [(fmz, sp)];
2.134 Iterator 1; moveActiveRoot 1;
2.135 refFormula 1 (get_pos 1 1);
2.136 @@ -936,7 +936,7 @@
2.137 [Given ["equality (1+-1*2+x=(0::real))", "solveFor x"],
2.138 Find ["solutions L"]],
2.139 Pbl,
2.140 - ("Test", ["linear","univariate","equation","test"],
2.141 + ("Test", ["LINEAR","univariate","equation","test"],
2.142 ["Test","solve_linear"]));
2.143 autoCalculate 1 CompleteCalc;
2.144 refFormula 1 (get_pos 1 1);
2.145 @@ -1074,7 +1074,7 @@
2.146 CalcTree (*start of calculation, return No.1*)
2.147 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
2.148 ("Test",
2.149 - ["linear","univariate","equation","test"],
2.150 + ["LINEAR","univariate","equation","test"],
2.151 ["Test","solve_linear"]))];
2.152 Iterator 1; moveActiveRoot 1;
2.153
3.1 --- a/test/Tools/isac/Interpret/calchead.sml Thu Nov 21 17:31:20 2013 +0100
3.2 +++ b/test/Tools/isac/Interpret/calchead.sml Thu Nov 21 18:12:17 2013 +0100
3.3 @@ -329,11 +329,11 @@
3.4 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.5 (*...copied from stac2tac_*)
3.6 str2term (
3.7 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
3.8 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.9 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
3.10 " REAL_LIST [c, c_2]]");
3.11 val ags = isalist2list ags';
3.12 -val pI = ["linear","system"];
3.13 +val pI = ["LINEAR","system"];
3.14 val pats = (#ppc o get_pbt) pI;
3.15 "-a1-----------------------------------------------------";
3.16 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
3.17 @@ -354,11 +354,11 @@
3.18 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.19 (*...copied from stac2tac_*)
3.20 str2term (
3.21 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
3.22 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.23 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
3.24 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
3.25 val ags = isalist2list ags';
3.26 -val pI = ["linear","system"];
3.27 +val pI = ["LINEAR","system"];
3.28 val pats = (#ppc o get_pbt) pI;
3.29 "-b1-----------------------------------------------------";
3.30 val xxx = match_ags @{theory "Isac"} pats ags;
3.31 @@ -380,10 +380,10 @@
3.32 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.33 (*...copied from stac2tac_*)
3.34 str2term (
3.35 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
3.36 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.37 " [REAL_LIST [c, c_2]]");
3.38 val ags = isalist2list ags';
3.39 -val pI = ["linear","system"];
3.40 +val pI = ["LINEAR","system"];
3.41 val pats = (#ppc o get_pbt) pI;
3.42 (*============ inhibit exn AK110726 ==============================================
3.43 val xxx - match_ags (theory "EqSystem") pats ags;
3.44 @@ -420,11 +420,11 @@
3.45 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.46 (*...copied from stac2tac_*)
3.47 str2term (
3.48 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
3.49 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.50 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
3.51 " REAL_LIST [c, c_2]]");
3.52 val ags = isalist2list ags';
3.53 -val pI = ["linear","system"];
3.54 +val pI = ["LINEAR","system"];
3.55 val pats = (#ppc o get_pbt) pI;
3.56 "-a1-----------------------------------------------------";
3.57 (*match_ags = fn : theory -> pat list -> term list -> ori list*)
3.58 @@ -445,11 +445,11 @@
3.59 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.60 (*...copied from stac2tac_*)
3.61 str2term (
3.62 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
3.63 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.64 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
3.65 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
3.66 val ags = isalist2list ags';
3.67 -val pI = ["linear","system"];
3.68 +val pI = ["LINEAR","system"];
3.69 val pats = (#ppc o get_pbt) pI;
3.70 "-b1-----------------------------------------------------";
3.71 val xxx = match_ags @{theory "Isac"} pats ags;
3.72 @@ -471,10 +471,10 @@
3.73 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.74 (*...copied from stac2tac_*)
3.75 str2term (
3.76 - "SubProblem (EqSystem', [linear, system], [no_met]) " ^
3.77 + "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.78 " [REAL_LIST [c, c_2]]");
3.79 val ags = isalist2list ags';
3.80 -val pI = ["linear","system"];
3.81 +val pI = ["LINEAR","system"];
3.82 val pats = (#ppc o get_pbt) pI;
3.83 (*============ inhibit exn AK110726 ==============================================
3.84 val xxx - match_ags (theory "EqSystem") pats ags;
3.85 @@ -600,7 +600,7 @@
3.86 vars' ~~ vals;
3.87 (*[("e_e", [x+1=2), ("v_v", x)] OLD: [("e_", [x+1=2), ("v_", x)]*)
3.88 (assoc (vars'~~vals, cy'));
3.89 -(*SOME (Free ("x", "RealDef.real")) : term option*)
3.90 +(*SOME (Free ("x", "Real.real")) : term option*)
3.91 val cy_ext = (free2str o the) (assoc (vars'~~vals, cy'))^"_"^ext;
3.92 (*x_i*)
3.93 "-----------------continue step through code match_ags---";
3.94 @@ -655,7 +655,7 @@
3.95 @{term "equalities"}; type_of @{term "[x_1+1=2,x_2=0]"};
3.96 @{term "solveForVars"}; type_of @{term "[x_1,x_2]::real list"};
3.97 @{term "solution"}; type_of @{term "ss''' :: bool list"};
3.98 -(*the model-pattern for ["linear", "system"], is_copy_named are filter_out*)
3.99 +(*the model-pattern for ["LINEAR", "system"], is_copy_named are filter_out*)
3.100 val pbt = [("#Given", (@{term "equalities"}, @{term "e_s :: bool list"})),
3.101 ("#Given", (@{term "solveForVars v_s"}, @{term "v_s :: bool list"} ))];
3.102 (*the model specific for an example*)
3.103 @@ -704,32 +704,32 @@
3.104 probl = [], branch = TransitiveB,
3.105 origin =
3.106 ([(1, [1], "#Given",
3.107 - Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
3.108 + Const ("Descript.functionTerm", "Real.real => Tools.una"),
3.109 [Const ("op +",
3.110 - "[RealDef.real, RealDef.real] => RealDef.real") $
3.111 + "["Real.real, "Real.real] => "Real.real") $
3.112 (Const ("Atools.pow",
3.113 - "[RealDef.real, RealDef.real] => RealDef.real") $
3.114 - Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
3.115 - Free ("1", "RealDef.real")]),
3.116 + "["Real.real, "Real.real] => "Real.real") $
3.117 + Free ("x", "Real.real") $ Free ("2", "Real.real")) $
3.118 + Free ("1", "Real.real")]),
3.119 (2, [1], "#Given",
3.120 - Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
3.121 - [Free ("x", "RealDef.real")]),
3.122 + Const ("Integrate.integrateBy", "Real.real => Tools.una"),
3.123 + [Free ("x", "Real.real")]),
3.124 (3, [1], "#Find",
3.125 - Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
3.126 - [Free ("FF", "RealDef.real")])],
3.127 + Const ("Integrate.antiDerivative", "Real.real => Tools.una"),
3.128 + [Free ("FF", "Real.real")])],
3.129 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
3.130 Const ("Integrate.Integrate",
3.131 - "(RealDef.real, RealDef.real) * => RealDef.real") $
3.132 + "("Real.real, "Real.real) * => "Real.real") $
3.133 (Const ("Product_Type.Pair",
3.134 - "[RealDef.real, RealDef.real]
3.135 - => (RealDef.real, RealDef.real) *") $
3.136 + "["Real.real, "Real.real]
3.137 + => ("Real.real, "Real.real) *") $
3.138 (Const ("op +",
3.139 - "[RealDef.real, RealDef.real] => RealDef.real") $
3.140 + "["Real.real, "Real.real] => "Real.real") $
3.141 (Const ("Atools.pow",
3.142 - "[RealDef.real, RealDef.real] => RealDef.real") $
3.143 - Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
3.144 - Free ("1", "RealDef.real")) $
3.145 - Free ("x", "RealDef.real"))),
3.146 + "["Real.real, "Real.real] => "Real.real") $
3.147 + Free ("x", "Real.real") $ Free ("2", "Real.real")) $
3.148 + Free ("1", "Real.real")) $
3.149 + Free ("x", "Real.real"))),
3.150 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
3.151 []) : ptree*)
3.152 "----- WN101007 worked until here (checked same as isac2002) ---";
3.153 @@ -765,44 +765,44 @@
3.154 ("e_domID", ["e_pblID"], ["e_metID"]), probl =
3.155 [(0, [], false, "#Given",
3.156 Inc ((Const ("Descript.functionTerm",
3.157 - "RealDef.real => Tools.una"),[]),
3.158 + "Real.real => Tools.una"),[]),
3.159 (Const ("empty", "'a"), []))),
3.160 (0, [], false, "#Given",
3.161 Inc ((Const ("Integrate.integrateBy",
3.162 - "RealDef.real => Tools.una"),[]),
3.163 + "Real.real => Tools.una"),[]),
3.164 (Const ("empty", "'a"), []))),
3.165 (0, [], false, "#Find",
3.166 Inc ((Const ("Integrate.antiDerivative",
3.167 - "RealDef.real => Tools.una"),[]),
3.168 + "Real.real => Tools.una"),[]),
3.169 (Const ("empty", "'a"), [])))],
3.170 branch = TransitiveB, origin =
3.171 ([(1, [1], "#Given",
3.172 - Const ("Descript.functionTerm", "RealDef.real => Tools.una"),
3.173 + Const ("Descript.functionTerm", "Real.real => Tools.una"),
3.174 [Const ("op +",
3.175 - "[RealDef.real, RealDef.real] => RealDef.real") $
3.176 + "["Real.real, "Real.real] => "Real.real") $
3.177 (Const ("Atools.pow",
3.178 - "[RealDef.real, RealDef.real] => RealDef.real") $
3.179 - Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
3.180 - Free ("1", "RealDef.real")]),
3.181 + "["Real.real, "Real.real] => "Real.real") $
3.182 + Free ("x", "Real.real") $ Free ("2", "Real.real")) $
3.183 + Free ("1", "Real.real")]),
3.184 (2, [1], "#Given",
3.185 - Const ("Integrate.integrateBy", "RealDef.real => Tools.una"),
3.186 - [Free ("x", "RealDef.real")]),
3.187 + Const ("Integrate.integrateBy", "Real.real => Tools.una"),
3.188 + [Free ("x", "Real.real")]),
3.189 (3, [1], "#Find",
3.190 - Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
3.191 - [Free ("FF", "RealDef.real")])],
3.192 + Const ("Integrate.antiDerivative", "Real.real => Tools.una"),
3.193 + [Free ("FF", "Real.real")])],
3.194 ("Integrate", ["integrate", "function"], ["diff", "integration"]),
3.195 Const ("Integrate.Integrate",
3.196 - "(RealDef.real, RealDef.real) * => RealDef.real") $
3.197 + "("Real.real, "Real.real) * => "Real.real") $
3.198 (Const ("Product_Type.Pair",
3.199 - "[RealDef.real, RealDef.real]
3.200 - => (RealDef.real, RealDef.real) *") $
3.201 + "["Real.real, "Real.real]
3.202 + => ("Real.real, "Real.real) *") $
3.203 (Const ("op +",
3.204 - "[RealDef.real, RealDef.real] => RealDef.real") $
3.205 + "["Real.real, "Real.real] => "Real.real") $
3.206 (Const ("Atools.pow",
3.207 - "[RealDef.real, RealDef.real] => RealDef.real") $
3.208 - Free ("x", "RealDef.real") $ Free ("2", "RealDef.real")) $
3.209 - Free ("1", "RealDef.real")) $
3.210 - Free ("x", "RealDef.real"))),
3.211 + "["Real.real, "Real.real] => "Real.real") $
3.212 + Free ("x", "Real.real") $ Free ("2", "Real.real")) $
3.213 + Free ("1", "Real.real")) $
3.214 + Free ("x", "Real.real"))),
3.215 ostate = Incomplete, result = (Const ("empty", "'a"), [])},
3.216 []) : ptree*)
3.217 "----- WN101007 ptree checked same as isac2002, diff. in nxt --- REPAIRED";
3.218 @@ -825,8 +825,8 @@
3.219 "----- this fmz is transformed to this internal format (TERM --> Pure.term):";
3.220 val ([(1, [1], "#undef", _, [Const ("Pure.term", _ (*"'a \<Rightarrow> prop"*)) $ _]),
3.221 (*#############################^^^^^^^^^ defined by Isabelle*)
3.222 - (2, [1], "#Find", Const ("Simplify.normalform", _ (*"RealDef.real \<Rightarrow> Tools.una"*)),
3.223 - [Free ("N", _ (*"RealDef.real"*))])],
3.224 + (2, [1], "#Find", Const ("Simplify.normalform", _ (*"Real.real \<Rightarrow> Tools.una"*)),
3.225 + [Free ("N", _ (*"Real.real"*))])],
3.226 _ ) = prep_ori fmz thy ((#ppc o get_pbt) pI);
3.227 "#undef means: the element with description TERM in fmz did not match ";
3.228 "with any element of pbl (fetched by pI), because there we have Simplify.Term";
4.1 --- a/test/Tools/isac/Interpret/ctree.sml Thu Nov 21 17:31:20 2013 +0100
4.2 +++ b/test/Tools/isac/Interpret/ctree.sml Thu Nov 21 18:12:17 2013 +0100
4.3 @@ -591,7 +591,7 @@
4.4 CalcTree (*start of calculation, return No.1*)
4.5 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
4.6 ("Test",
4.7 - ["linear","univariate","equation","test"],
4.8 + ["LINEAR","univariate","equation","test"],
4.9 ["Test","solve_linear"]))];
4.10 Iterator 1; moveActiveRoot 1;
4.11 autoCalculate 1 CompleteCalcHead;
4.12 @@ -974,7 +974,7 @@
4.13 val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));
4.14 case (term2str form, tac, terms2strs asm) of
4.15 ("-1 + x = 0",
4.16 - Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
4.17 + Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
4.18 []) => ()
4.19 | _ => error "diff.behav.in ctree.sml: pt_extract ([2], Res)";
4.20
4.21 @@ -995,7 +995,7 @@
4.22
4.23 val (Form form, SOME tac, asm) = pt_extract (pt, ([3,2], Res));
4.24 case (term2str form, tac, terms2strs asm) of
4.25 - ("x = 1", Check_Postcond ["linear", "univariate", "equation", "test"],
4.26 + ("x = 1", Check_Postcond ["LINEAR", "univariate", "equation", "test"],
4.27 []) => ()
4.28 | _ => error "diff.behav.in ctree.sml: pt_extract ([3,2], Res)";
4.29
5.1 --- a/test/Tools/isac/Interpret/inform.sml Thu Nov 21 17:31:20 2013 +0100
5.2 +++ b/test/Tools/isac/Interpret/inform.sml Thu Nov 21 18:12:17 2013 +0100
5.3 @@ -220,7 +220,7 @@
5.4
5.5 fetchProposedTactic 1;
5.6 val (_,(tac,_,_)::_) = get_calc 1;
5.7 - if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()
5.8 + if tac = Check_Postcond ["LINEAR", "univariate", "equation", "test"] then ()
5.9 else error "inform.sml: diff.behav.appendFormula: Res + late d 2";
5.10 autoCalculate 1 CompleteCalc;
5.11 val ((pt,_),_) = get_calc 1;
6.1 --- a/test/Tools/isac/Interpret/mathengine.sml Thu Nov 21 17:31:20 2013 +0100
6.2 +++ b/test/Tools/isac/Interpret/mathengine.sml Thu Nov 21 18:12:17 2013 +0100
6.3 @@ -200,7 +200,7 @@
6.4 refineProblem 1 ([1],Res) "pbl_equ_univ"
6.5 (*gives "pbl_equ_univ_rat" correct*);
6.6
6.7 -refineProblem 1 ([1],Res) (pblID2guh ["linear","univariate","equation"])
6.8 +refineProblem 1 ([1],Res) (pblID2guh ["LINEAR","univariate","equation"])
6.9 (*gives "pbl_equ_univ_lin" incorrect*);
6.10
6.11
7.1 --- a/test/Tools/isac/Interpret/me.sml Thu Nov 21 17:31:20 2013 +0100
7.2 +++ b/test/Tools/isac/Interpret/me.sml Thu Nov 21 18:12:17 2013 +0100
7.3 @@ -343,7 +343,7 @@
7.4 val (p,_,f,nxt,_,pt) = CalcTreeTEST
7.5 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
7.6 ("Test",
7.7 - ["linear","univariate","equation","test"],
7.8 + ["LINEAR","univariate","equation","test"],
7.9 ["Test","solve_linear"]))];
7.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
7.12 @@ -379,7 +379,7 @@
7.13 CalcTree (*start of calculation, return No.1*)
7.14 [(["equality (1+-1*2+x=(0::real))", "solveFor x","solutions L"],
7.15 ("Test",
7.16 - ["linear","univariate","equation","test"],
7.17 + ["LINEAR","univariate","equation","test"],
7.18 ["Test","solve_linear"]))];
7.19 Iterator 1; moveActiveRoot 1;
7.20
8.1 --- a/test/Tools/isac/Interpret/mstools.sml Thu Nov 21 17:31:20 2013 +0100
8.2 +++ b/test/Tools/isac/Interpret/mstools.sml Thu Nov 21 18:12:17 2013 +0100
8.3 @@ -116,7 +116,7 @@
8.4 val SOME known_x = parseNEW ctxt "x+y+z";
8.5 val SOME unknown = parseNEW ctxt "xa+b+c";
8.6
8.7 -if type_of known_x = Type ("RealDef.real",[]) then ()
8.8 +if type_of known_x = Type ("Real.real",[]) then ()
8.9 else error "x+1=2 after start root-pbl wrong type-inference from known x";
8.10 if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
8.11 else error "x+1=2 after start root-pbl wrong type-inference for unknowns a,b,c";
8.12 @@ -134,14 +134,14 @@
8.13 else error "x+1=2 after start root-met no precondition";
8.14
8.15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.16 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
8.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
8.18 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.19
8.20 "=(3)= variables known from arguments of (sub-)method provide type-inference for further input";
8.21 val ctxt = get_ctxt pt p;
8.22 val SOME known_x = parseNEW ctxt "x+y+z";
8.23 val SOME unknown = parseNEW ctxt "a+b+c";
8.24 -if type_of known_x = Type ("RealDef.real",[]) then ()
8.25 +if type_of known_x = Type ("Real.real",[]) then ()
8.26 else error "x+1=2 after start root-pbl wrong type-inference for known x";
8.27 if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
8.28 else error "x+1=2 after start root-pbl wrong type-inference for unknowns a,b,c";
8.29 @@ -167,7 +167,7 @@
8.30 val ctxt = insert_assumptions [str2term "x < sub_asm_out", str2term "a < sub_asm_local"] cres;
8.31 val pt = update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt));
8.32
8.33 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
8.34 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR","univariate", ...]) *);
8.35 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
8.36
8.37 "=(5)= transfer non-local assumptions and result from sub-method to root-method." ^
9.1 --- a/test/Tools/isac/Interpret/ptyps.sml Thu Nov 21 17:31:20 2013 +0100
9.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Thu Nov 21 18:12:17 2013 +0100
9.3 @@ -361,7 +361,7 @@
9.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.5 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Add_Find", Add_Find "solutions L")*)
9.6
9.7 -val nxt = ("Specify_Problem", Specify_Problem ["linear","univariate","equation","test"]);
9.8 +val nxt = ("Specify_Problem", Specify_Problem ["LINEAR","univariate","equation","test"]);
9.9 (*=== specify a not-matching problem ------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
9.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.11 if f = Form' (PpcKF (0, EdUndef, 0, Nundef, (Problem [],
9.12 @@ -375,7 +375,7 @@
9.13 else error "--- Refine_Problem broken 1";
9.14 (*ML> f;
9.15 val it = Form' (PpcKF (0,EdUndef,0,Nundef,
9.16 - (Problem ["linear","univariate","equation","test"], <<<<<===== diff.to above WN120313
9.17 + (Problem ["LINEAR","univariate","equation","test"], <<<<<===== diff.to above WN120313
9.18 {Find=[Incompl "solutions []"],
9.19 Given=[Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)",
9.20 Correct "solveFor x"],Relate=[],
9.21 @@ -389,7 +389,7 @@
9.22 val (p,_,f,nxt,_,pt) = (me nxt p c pt) (*handle e => OldGoals.print_exn e*);
9.23 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.24 (*val nxt = ("Empty_Tac",Empty_Tac)
9.25 -... Refine_Problem ["linear"..] fails internally 040312: works!?!*)
9.26 +... Refine_Problem ["LINEAR"..] fails internally 040312: works!?!*)
9.27
9.28 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
9.29 (*=== refine problem -----------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
9.30 @@ -406,10 +406,10 @@
9.31 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.32 (*nxt = ("Rewrite_Set", Rewrite_Set "Test_simplify")*)
9.33 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.34 -(*Subproblem ("Test", ["linear", "univariate", "equation", "test"]*)
9.35 +(*Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]*)
9.36
9.37 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.38 -(*nxt = Model_Problem ["linear","univariate","equation","test"]*)
9.39 +(*nxt = Model_Problem ["LINEAR","univariate","equation","test"]*)
9.40 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.41 (*nxt = ("Add_Given", Add_Given "equality (-6 + 3 * x = 0)"*)
9.42 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.43 @@ -417,12 +417,12 @@
9.44 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.45 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.46 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.47 -(*nxt = Specify_Problem ["linear","univariate","equation","test"])*)
9.48 +(*nxt = Specify_Problem ["LINEAR","univariate","equation","test"])*)
9.49 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.50 (*xt = ("Specify_Method", Specify_Method ["Test", "solve_linear"])*)
9.51 val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]);
9.52 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.53 -(*("Specify_Problem", Specify_Problem ["linear", "univariate", ...])*)
9.54 +(*("Specify_Problem", Specify_Problem ["LINEAR", "univariate", ...])*)
9.55 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.56 (*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
9.57 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.58 @@ -432,7 +432,7 @@
9.59 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.60 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
9.61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.62 -(*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*)
9.63 +(*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","eq*)
9.64 val (p,_,f,nxt,_,pt) = me nxt p c pt;
9.65 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
9.66 val (p,_,f,nxt,_,pt) = me nxt p c pt;
10.1 --- a/test/Tools/isac/Interpret/rewtools.sml Thu Nov 21 17:31:20 2013 +0100
10.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Thu Nov 21 18:12:17 2013 +0100
10.3 @@ -431,7 +431,7 @@
10.4 CalcTree
10.5 [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
10.6 ("Test",
10.7 - ["linear","univariate","equation","test"],
10.8 + ["LINEAR","univariate","equation","test"],
10.9 ["Test","solve_linear"]))];
10.10 Iterator 1; moveActiveRoot 1;
10.11 autoCalculate 1 CompleteCalcHead;
10.12 @@ -454,7 +454,7 @@
10.13 CalcTree
10.14 [(["equality (1+-1*2+x=(0::real))", "solveFor x", "solutions L"],
10.15 ("Test",
10.16 - ["linear","univariate","equation","test"],
10.17 + ["LINEAR","univariate","equation","test"],
10.18 ["Test","solve_linear"]))];
10.19 Iterator 1; moveActiveRoot 1;
10.20 autoCalculate 1 CompleteCalc;
11.1 --- a/test/Tools/isac/Interpret/script.sml Thu Nov 21 17:31:20 2013 +0100
11.2 +++ b/test/Tools/isac/Interpret/script.sml Thu Nov 21 18:12:17 2013 +0100
11.3 @@ -152,7 +152,7 @@
11.4 ("Illegal type for constant \"op =\" :: \"[real, bool] => bool\"",
11.5 [],
11.6 [Const ("HOL.Trueprop", "bool => prop") $
11.7 - (Const ("HOL.eq", "[RealDef.real, bool] => bool") $ ... $ ...)])
11.8 + (Const ("HOL.eq", "["Real.real, bool] => bool") $ ... $ ...)])
11.9 raised
11.10 ... this was because eval_argument_in took "argument_in (lhs (M_b 0 = 0))"
11.11 ie. the argument had not been simplified before ^^^^^^^^^^^^^^^
11.12 @@ -300,7 +300,7 @@
11.13 val (pt, p) = case locatetac tac (pt,p) of
11.14 ("ok", (_, _, ptp)) => ptp | _ => error "script.sml locatetac";
11.15 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
11.16 -val pIopt = get_pblID (pt,ip); (*SOME ["linear", "univariate", "equation", "test"]*)
11.17 +val pIopt = get_pblID (pt,ip); (*SOME ["LINEAR", "univariate", "equation", "test"]*)
11.18 tacis; (*= []*)
11.19 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)); (*= false*)
11.20 "~~~~~ fun nxt_solve_, args:"; val (ptp as (pt, pos as (p, p_))) = (pt, ip);
11.21 @@ -313,7 +313,7 @@
11.22 val Appy (m', scrst as (_,_,_,v,_,_)) = nstep_up thy ptp sc E l Skip_ a v;
11.23 "~~~~~ dont like to go into nstep_up...";
11.24 val t = str2term ("SubProblem" ^
11.25 - "(Test', [linear, univariate, equation, test], [Test, solve_linear])" ^
11.26 + "(Test', [LINEAR, univariate, equation, test], [Test, solve_linear])" ^
11.27 "[BOOL (-1 + x = 0), REAL x]");
11.28 val (tac, tac_) = stac2tac_ pt @{theory "Isac"} t; (*WAS stac2tac_ TODO: no match for SubProblem*)
11.29 case tac_ of
11.30 @@ -419,7 +419,7 @@
11.31
11.32 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
11.33 val (p'''', pt'''') = (p, pt);
11.34 -f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["linear", "univariate", "equation", "test"]);
11.35 +f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]);
11.36 val (p, p_) = p(* = ([2], Res)*);
11.37 val (srls, (ScrState scrstate, ctxt), Prog sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
11.38 val (env, loc_, curry_arg, res, Safe, false) = scrstate;
11.39 @@ -493,7 +493,7 @@
11.40
11.41 val tacs = sel_rules pt ([1],Res);
11.42 if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
11.43 - Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
11.44 + Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
11.45 Check_elementwise "Assumptions"] then ()
11.46 else error "script.sml: diff.behav. in sel_rules ([1],Res)";
11.47
11.48 @@ -508,7 +508,7 @@
11.49
11.50 val tacs = sel_rules pt ([3],Res);
11.51 if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
11.52 - Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
11.53 + Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
11.54 Check_elementwise "Assumptions"] then ()
11.55 else error "script.sml: diff.behav. in sel_rules ([3],Res)";
11.56
11.57 @@ -535,14 +535,14 @@
11.58 val ((pt, _), _) = get_calc cI;
11.59 (*version 1:*)
11.60 if sel_rules pt p = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
11.61 - Subproblem ("Test", ["linear", "univariate", "equation", "test"]),
11.62 + Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
11.63 Check_elementwise "Assumptions"] then ()
11.64 else error "fetchApplicableTactics ([1],Res) changed";
11.65 (*version 2:*)
11.66 (*WAS:
11.67 sel_appl_atomic_tacs pt p;
11.68 ...
11.69 -### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["linear","univariate","equation","test"])'
11.70 +### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
11.71 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
11.72 *)
11.73
11.74 @@ -568,7 +568,7 @@
11.75 (*WN120611 stopped and took version 1 again for fetchApplicableTactics !
11.76 (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
11.77 ...
11.78 -### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["linear","univariate","equation","test"])'
11.79 +### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
11.80 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
11.81 *)
11.82
12.1 --- a/test/Tools/isac/Knowledge/build_thydata.sml Thu Nov 21 17:31:20 2013 +0100
12.2 +++ b/test/Tools/isac/Knowledge/build_thydata.sml Thu Nov 21 18:12:17 2013 +0100
12.3 @@ -282,7 +282,8 @@
12.4 "-------- hard-coded val rlsthmsNOTisac -----------------";
12.5 "-------- hard-coded val rlsthmsNOTisac -----------------";
12.6 "-------- hardcode val rlsthmsNOTisac -------------------";
12.7 -(*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac:*)
12.8 +(*WN120319: since num_str destoys derivation_name, we hardcode rlsthmsNOTisac:
12.9 + WN131121: at least ERROR Unknown fact "Real.order_refl"*)
12.10 val rlsthmsNOTisac =
12.11 [("HOL.refl", (prop_of o num_str) @{thm refl}),
12.12 ("Fun.o_apply", (prop_of o num_str) @{thm o_apply}),
12.13 @@ -307,10 +308,10 @@
12.14 ("Groups.monoid_add_class.add_0_right", (prop_of o num_str) @{thm add_0_right}),
12.15 ("Rings.division_ring_class.divide_zero_left", (prop_of o num_str) @{thm divide_zero_left}),
12.16 (*###("sym_mult_assoc", "?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1")*)
12.17 - ("RealDef.order_refl", (prop_of o num_str) @{thm order_refl}),
12.18 + ("Real.order_refl", (prop_of o num_str) @{thm order_refl}),
12.19 ("Groups.group_add_class.minus_minus", (prop_of o num_str) @{thm minus_minus}),
12.20 - ("RealDef.mult_commute", (prop_of o num_str) @{thm mult_commute }),
12.21 - ("RealDef.mult_assoc", (prop_of o num_str) @{thm mult_assoc}),
12.22 + ("Real.mult_commute", (prop_of o num_str) @{thm mult_commute }),
12.23 + ("Real.mult_assoc", (prop_of o num_str) @{thm mult_assoc}),
12.24 ("Groups.ab_semigroup_add_class.add_commute", (prop_of o num_str) @{thm add_commute}),
12.25 ("Groups.ab_semigroup_add_class.add_left_commute", (prop_of o num_str) @{thm add_left_commute}),
12.26 ("Groups.semigroup_add_class.add_assoc", (prop_of o num_str) @{thm add_assoc}),
13.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Nov 21 17:31:20 2013 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Thu Nov 21 18:12:17 2013 +0100
13.3 @@ -82,7 +82,7 @@
13.4 val ctxt = get_ctxt pt pos;
13.5 val SOME known_x = parseNEW ctxt "x+z+z"; (*x has declare_constraints to real*)
13.6 val SOME unknown = parseNEW ctxt "a+b+c";
13.7 -if type_of known_x = Type ("RealDef.real",[]) then ()
13.8 +if type_of known_x = Type ("Real.real",[]) then ()
13.9 else error "x+1=2 after start root-pbl wrong type-inference for known_x";
13.10 if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
13.11 else error "x+1=2 after start root-pbl wrong type-inference for unknown";
14.1 --- a/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Nov 21 17:31:20 2013 +0100
14.2 +++ b/test/Tools/isac/Minisubpbl/400-start-meth-subpbl.sml Thu Nov 21 18:12:17 2013 +0100
14.3 @@ -20,7 +20,7 @@
14.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
14.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.7 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
14.8 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
14.9 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.10 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
14.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.1 --- a/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Thu Nov 21 17:31:20 2013 +0100
15.2 +++ b/test/Tools/isac/Minisubpbl/490-nxt-Check_Postcond.sml Thu Nov 21 18:12:17 2013 +0100
15.3 @@ -20,7 +20,7 @@
15.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
15.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.7 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
15.8 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
15.9 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.10 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15.12 @@ -78,7 +78,7 @@
15.13 val (pt,c) = append_result pt p l (scval, (*map str2term*) asm) Complete;
15.14 (*----------------------------------------############### changed*)
15.15
15.16 -val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["linear","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
15.17 -if nxt = ("Check_Postcond", Check_Postcond ["linear", "univariate", "equation", "test"])
15.18 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Check_Postcond ["LINEAR","uval (srls, is, sc) = from_pblobj_or_detail' thy' (p,p_) pt; (*is: which ctxt?*)nivariate", ...]) *);
15.19 +if nxt = ("Check_Postcond", Check_Postcond ["LINEAR", "univariate", "equation", "test"])
15.20 then () else error "450-nxt-Check_Postcond broken"
15.21
16.1 --- a/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Thu Nov 21 17:31:20 2013 +0100
16.2 +++ b/test/Tools/isac/Minisubpbl/500-met-sub-to-root.sml Thu Nov 21 18:12:17 2013 +0100
16.3 @@ -20,7 +20,7 @@
16.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
16.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.7 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
16.8 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
16.9 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.10 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16.12 @@ -31,7 +31,7 @@
16.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "solve_linear"]*)
16.14 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set_Inst isolate_bdv*);
16.15 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Rewrite_Set "Test_simplify"*);
16.16 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
16.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR","univariate", ...]) *);
16.18 val (pt''', p''') = (pt, p);
16.19
16.20 (*WN110521 worked without testing*)
17.1 --- a/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Nov 21 17:31:20 2013 +0100
17.2 +++ b/test/Tools/isac/Minisubpbl/530-error-Check_Elementwise.sml Thu Nov 21 18:12:17 2013 +0100
17.3 @@ -21,7 +21,7 @@
17.4 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
17.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.6 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.7 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["linear", "univariate", "equation", "test"]*)
17.8 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Subp ["LINEAR", "univariate", "equation", "test"]*)
17.9 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.10 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17.12 @@ -41,7 +41,7 @@
17.13 val ctxt = get_ctxt pt p;
17.14 val SOME t = parseNEW ctxt "Check_elementwise [x = 1] {(v_v::real). Assumptions}";
17.15 get_loc pt p |> snd |> is_e_ctxt; (*false*)
17.16 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["linear","univariate", ...]) *);
17.17 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Check_Postcond ["LINEAR","univariate", ...]) *);
17.18
17.19 val (pt'''', p'''') = (pt, p);
17.20 "~~~~~ fun me, args:"; val (_,tac) = nxt;
18.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Thu Nov 21 17:31:20 2013 +0100
18.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Thu Nov 21 18:12:17 2013 +0100
18.3 @@ -430,7 +430,7 @@
18.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.7 -(*val nxt = Subproblem ("Test",["linear","univariate","equation","test"*)
18.8 +(*val nxt = Subproblem ("Test",["LINEAR","univariate","equation","test"*)
18.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.12 @@ -439,7 +439,7 @@
18.13 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.14 val (p,_,f,nxt,_,pt) = me nxt p c pt;
18.15 (*val nxt =
18.16 - ("Check_Postcond",Check_Postcond ["linear","univariate","equation","test"])*)
18.17 + ("Check_Postcond",Check_Postcond ["LINEAR","univariate","equation","test"])*)
18.18 val asms = get_assumptions_ pt p;
18.19 if asms = [] then ()
18.20 else error "scriptnew.sml diff.behav. in sqrt assumptions 3";
19.1 --- a/test/Tools/isac/OLDTESTS/subp-rooteq.sml Thu Nov 21 17:31:20 2013 +0100
19.2 +++ b/test/Tools/isac/OLDTESTS/subp-rooteq.sml Thu Nov 21 18:12:17 2013 +0100
19.3 @@ -99,7 +99,7 @@
19.4 ########## OK*)
19.5 p;
19.6 writeln(istate2str (fst (get_istate pt ([3],Frm))));
19.7 -(*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*)
19.8 +(*val nxt = ("Model_Problem",Model_Problem ["LINEAR","univariate","equation"]*)
19.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.10 (*val nxt = ("Add_Given",Add_Given "equality (-1 + x = 0)") *)
19.11 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.12 @@ -109,7 +109,7 @@
19.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.14 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
19.15 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.16 -(*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
19.17 +(*("Specify_Problem",Specify_Problem ["LINEAR","univariate","equation"])*)
19.18 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.19 (*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
19.20 val Prog sc = (#scr o get_met) ["Test","solve_linear"];
19.21 @@ -122,7 +122,7 @@
19.22 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
19.23
19.24 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.25 -(*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*)
19.26 +(*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","eq*)
19.27
19.28 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.29 p;
19.30 @@ -142,7 +142,7 @@
19.31 val fmz = ["equality (1+-1*2+x=(0::real))",
19.32 "solveFor x","solutions L"];
19.33 val (dI',pI',mI') =
19.34 - ("Test",["linear","univariate","equation","test"],
19.35 + ("Test",["LINEAR","univariate","equation","test"],
19.36 ["Test","solve_linear"]);
19.37
19.38 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
19.39 @@ -257,9 +257,9 @@
19.40 (*"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"*)
19.41 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.42 (*"-4 + x = 0"
19.43 - val nxt =("Subproblem",Subproblem ("Test",["linear","univariate"...*)
19.44 + val nxt =("Subproblem",Subproblem ("Test",["LINEAR","univariate"...*)
19.45 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.46 -(*val nxt =("Model_Problem",Model_Problem ["linear","univariate"...*)
19.47 +(*val nxt =("Model_Problem",Model_Problem ["LINEAR","univariate"...*)
19.48 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.49 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.50
19.51 @@ -267,14 +267,14 @@
19.52 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.53 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
19.54 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.55 -(*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
19.56 +(*("Specify_Problem",Specify_Problem ["LINEAR","univariate","equation"])*)
19.57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.58 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.59 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.60 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.61 (*"x = 0 + -1 * -4", nxt Test_simplify*)
19.62 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.63 -(*"x = 4", nxt Check_Postcond ["linear","univariate","equation","test"]*)
19.64 +(*"x = 4", nxt Check_Postcond ["LINEAR","univariate","equation","test"]*)
19.65 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.66 (*"[x = 4]", nxt Check_elementwise "Assumptions"*)
19.67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.68 @@ -402,14 +402,14 @@
19.69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.70 (*"-4 + x = 0", nxt Subproblem ("Test",["univariate","equation"]))*)
19.71 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.72 -(*val nxt =("Model_Problem",Model_Problem ["linear","univar...*)
19.73 +(*val nxt =("Model_Problem",Model_Problem ["LINEAR","univar...*)
19.74 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.76 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.78 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
19.79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.80 -(*val nxt = ("Specify_Problem",Specify_Problem ["linear","univariate","equ*)
19.81 +(*val nxt = ("Specify_Problem",Specify_Problem ["LINEAR","univariate","equ*)
19.82 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.83 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
19.84 (*Apply_Method ("Test","norm_univar_equation")*)
19.85 @@ -514,7 +514,7 @@
19.86 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.87 (*val nxt = ("Subproblem",Subproblem ("Test",["univariate","equation"])*)
19.88 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.89 -(*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*)
19.90 +(*val nxt = ("Model_Problem",Model_Problem ["LINEAR","univariate","equation"]*)
19.91 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.92 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.93 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.94 @@ -526,7 +526,7 @@
19.95 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.96 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.97 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.98 -(*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","equatio*)
19.99 +(*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","equatio*)
19.100 val (p,_,f,nxt,_,pt) = me nxt p c pt;
19.101 (*val nxt = ("Check_Postcond",Check_Postcond ["normalize","univariate","equa*)
19.102 val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) =
20.1 --- a/test/Tools/isac/OLDTESTS/tacis.sml Thu Nov 21 17:31:20 2013 +0100
20.2 +++ b/test/Tools/isac/OLDTESTS/tacis.sml Thu Nov 21 18:12:17 2013 +0100
20.3 @@ -102,14 +102,14 @@
20.4 val str = pr_ptree pr_short pt;
20.5 writeln str;
20.6
20.7 - setNextTactic 1 (Subproblem ("Test",["linear","univariate",
20.8 + setNextTactic 1 (Subproblem ("Test",["LINEAR","univariate",
20.9 "equation","test"]));
20.10 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*solve (-1 + x = 0, x)*);
20.11 val ((pt,_),_) = get_calc 1;
20.12 val str = pr_ptree pr_short pt;
20.13 writeln str;
20.14
20.15 - setNextTactic 1 (Model_Problem (*["linear","univariate","equation","test"]*));
20.16 + setNextTactic 1 (Model_Problem (*["LINEAR","univariate","equation","test"]*));
20.17 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*equality ///*);
20.18
20.19 setNextTactic 1 (Add_Given "equality (-1 + x = 0)");
20.20 @@ -132,7 +132,7 @@
20.21 setNextTactic 1 (Rewrite_Set "Test_simplify");
20.22 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x = 1*);
20.23
20.24 - setNextTactic 1 (Check_Postcond ["linear","univariate","equation","test"]);
20.25 + setNextTactic 1 (Check_Postcond ["LINEAR","univariate","equation","test"]);
20.26 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*[x = 1]*);
20.27
20.28 setNextTactic 1 (Check_elementwise "Assumptions");
21.1 --- a/test/Tools/isac/ProgLang/calculate.sml Thu Nov 21 17:31:20 2013 +0100
21.2 +++ b/test/Tools/isac/ProgLang/calculate.sml Thu Nov 21 18:12:17 2013 +0100
21.3 @@ -169,7 +169,7 @@
21.4 val t = (term_of o the o (parse thy)) "6 / 2";
21.5 val rls = Test_simplify;
21.6 val (t,_) = the (rewrite_set_ thy false rls t);
21.7 -(*val t = Free ("3","RealDef.real") : term*)
21.8 +(*val t = Free ("3","Real.real") : term*)
21.9
21.10 val thy = "Test";
21.11 val t = "6 / 2";
22.1 --- a/test/Tools/isac/ProgLang/termC.sml Thu Nov 21 17:31:20 2013 +0100
22.2 +++ b/test/Tools/isac/ProgLang/termC.sml Thu Nov 21 18:12:17 2013 +0100
22.3 @@ -56,22 +56,22 @@
22.4 (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)
22.5 (*- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -*)
22.6 @{term "0::real"};
22.7 -(*Const ("Groups.zero_class.zero", "RealDef.real")*)
22.8 +(*Const ("Groups.zero_class.zero", "Real.real")*)
22.9 @{term "1::real"};
22.10 (**)
22.11 @{term "5::real"};
22.12 -(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.real") $
22.13 +(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $
22.14 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
22.15 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
22.16 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
22.17 @{term "-5::real"};
22.18 -(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.real") $
22.19 +(*Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $
22.20 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
22.21 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
22.22 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $ Const ("...", "Int.int"))))*)
22.23 @{term "- 5::real"};
22.24 -(*Const ("Groups.uminus_class.uminus", "RealDef.real \<Rightarrow> RealDef.real") $
22.25 - (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> RealDef.real") $
22.26 +(*Const ("Groups.uminus_class.uminus", "Real.real \<Rightarrow> "Real.real") $
22.27 + (Const ("Int.number_class.number_of", "Int.int \<Rightarrow> "Real.real") $
22.28 (Const ("Int.Bit1", "Int.int \<Rightarrow> Int.int") $
22.29 (Const ("Int.Bit0", "Int.int \<Rightarrow> Int.int") $
22.30 (Const ("Int.Bit1...", "Int.int \<Rightarrow> Int.int") $ Const (...)))))*)
22.31 @@ -225,9 +225,9 @@
22.32 print_depth 3; (*999*) insts;
22.33 (*val insts =
22.34 ({},
22.35 - {(("a", 0), ("RealDef.real", Free ("3", "RealDef.real"))),
22.36 - (("b", 0), ("RealDef.real", Free ("x", "RealDef.real"))),
22.37 - (("c", 0), ("RealDef.real", Free ("1", "RealDef.real")))})*)
22.38 + {(("a", 0), ("Real.real", Free ("3", "Real.real"))),
22.39 + (("b", 0), ("Real.real", Free ("x", "Real.real"))),
22.40 + (("c", 0), ("Real.real", Free ("1", "Real.real")))})*)
22.41
22.42 "----- throws exn MATCH...";
22.43 (* val t = str2term "x";
22.44 @@ -407,7 +407,7 @@
22.45 |> numbers_to_string;
22.46 val Var (("a", 0), ty) = t;
22.47 val Type (str, tys) = ty;
22.48 - if str = "RealDef.real" andalso tys = [] andalso ty = HOLogic.realT
22.49 + if str = "Real.real" andalso tys = [] andalso ty = HOLogic.realT
22.50 then ()
22.51 else error "termC.sml type-structure of \"?a :: real\" changed";
22.52
23.1 --- a/test/Tools/isac/Test_Some.thy Thu Nov 21 17:31:20 2013 +0100
23.2 +++ b/test/Tools/isac/Test_Some.thy Thu Nov 21 18:12:17 2013 +0100
23.3 @@ -1,6 +1,6 @@
23.4 theory Test_Some imports Isac
23.5 begin
23.6 -ML_file "Knowledge/diff.sml"
23.7 +ML_file "Interpret/mstools.sml"
23.8
23.9 section {* code for copy & paste ===============================================================*}
23.10 ML {*
23.11 @@ -26,12 +26,7 @@
23.12 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-*)
23.13 *}
23.14
23.15 -section {* ===================================================================================*}
23.16 -ML {*
23.17 -*} ML {*
23.18 -*} ML {*
23.19 -*} ML {*
23.20 -*}
23.21 +thm mult_commute
23.22
23.23 section {* ===================================================================================*}
23.24 ML {*
23.25 @@ -47,4 +42,11 @@
23.26 *} ML {*
23.27 *}
23.28
23.29 +section {* ===================================================================================*}
23.30 +ML {*
23.31 +*} ML {*
23.32 +*} ML {*
23.33 +*} ML {*
23.34 +*}
23.35 +
23.36 end
24.1 --- a/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Thu Nov 21 17:31:20 2013 +0100
24.2 +++ b/test/Tools/isac/xmlsrc/pbl-met-hierarchy.sml Thu Nov 21 18:12:17 2013 +0100
24.3 @@ -108,7 +108,7 @@
24.4 *)
24.5 (*Const
24.6 ("Biegelinie.Biegelinie",
24.7 - "(RealDef.real => RealDef.real) => Tools.una") : Term.term
24.8 + "("Real.real => "Real.real) => Tools.una") : Term.term
24.9 ..I.E. THE "Script.ID" _WAS_ ALREADY OCCUPIED BY A 'description'*)
24.10
24.11