1.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Wed Sep 08 16:45:27 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Wed Sep 08 16:47:22 2010 +0200
1.3 @@ -125,7 +125,7 @@
1.4 "----- d0_false ------";
1.5 (*EP*)
1.6 val fmz = ["equality ( 1 = 0)", "solveFor x","solutions L"];
1.7 -val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"],
1.8 +val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
1.9 ["PolyEq","solve_d0_polyeq_equation"]);
1.10 (*val p = e_pos';
1.11 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.12 @@ -143,7 +143,7 @@
1.13 "----- d0_true ------";
1.14 (*EP-7*)
1.15 val fmz = ["equality ( 0 = 0)", "solveFor x","solutions L"];
1.16 -val (dI',pI',mI') = ("PolyEq.thy",["degree_0","polynomial","univariate","equation"],
1.17 +val (dI',pI',mI') = ("PolyEq",["degree_0","polynomial","univariate","equation"],
1.18 ["PolyEq","solve_d0_polyeq_equation"]);
1.19 (*val p = e_pos'; val c = [];
1.20 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.21 @@ -167,7 +167,7 @@
1.22
1.23 "----- d2_pqformula1 ------!!!!";
1.24 val fmz = ["equality (-2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.25 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.26 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.27 (*val p = e_pos'; val c = [];
1.28 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.29 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.30 @@ -194,7 +194,7 @@
1.31 "----- d2_pqformula1_neg ------";
1.32 (*EP-8*)
1.33 val fmz = ["equality ( 2 +(-1)*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.34 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.35 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.36 (*val p = e_pos'; val c = [];
1.37 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.38 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.39 @@ -217,7 +217,7 @@
1.40
1.41 "----- d2_pqformula2 ------";
1.42 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.43 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.44 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.45 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.46 (*val p = e_pos'; val c = [];
1.47 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.48 @@ -237,7 +237,7 @@
1.49
1.50 "----- d2_pqformula2_neg ------";
1.51 val fmz = ["equality ( 2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.52 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.53 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.54 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.55 (*val p = e_pos'; val c = [];
1.56 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.57 @@ -258,7 +258,7 @@
1.58 "----- d2_pqformula3 ------";
1.59 (*EP-9*)
1.60 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.61 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.62 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.63 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.64 (*val p = e_pos'; val c = [];
1.65 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.66 @@ -277,7 +277,7 @@
1.67
1.68 "----- d2_pqformula3_neg ------";
1.69 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.70 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.71 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.72 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.73 (*val p = e_pos'; val c = [];
1.74 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.75 @@ -297,7 +297,7 @@
1.76
1.77 "----- d2_pqformula4 ------";
1.78 val fmz = ["equality (-2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.79 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.80 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.81 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.82 (*val p = e_pos'; val c = [];
1.83 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.84 @@ -316,7 +316,7 @@
1.85
1.86 "----- d2_pqformula4_neg ------";
1.87 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.88 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.89 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.90 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.91 (*val p = e_pos'; val c = [];
1.92 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.93 @@ -334,7 +334,7 @@
1.94
1.95 "----- d2_pqformula5 ------";
1.96 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.97 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.98 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.99 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.100 (*val p = e_pos'; val c = [];
1.101 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.102 @@ -353,7 +353,7 @@
1.103
1.104 "----- d2_pqformula6 ------";
1.105 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.106 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.107 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.108 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.109 (*val p = e_pos'; val c = [];
1.110 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.111 @@ -373,7 +373,7 @@
1.112 "----- d2_pqformula7 ------";
1.113 (*EP-10*)
1.114 val fmz = ["equality ( x + x^^^2 = 0)", "solveFor x","solutions L"];
1.115 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.116 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.117 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.118 (*val p = e_pos'; val c = [];
1.119 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.120 @@ -392,7 +392,7 @@
1.121
1.122 "----- d2_pqformula8 ------";
1.123 val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.124 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.125 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.126 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.127 (*val p = e_pos'; val c = [];
1.128 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.129 @@ -412,7 +412,7 @@
1.130
1.131 "----- d2_pqformula9 ------";
1.132 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.133 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.134 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.135 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.136 (*val p = e_pos'; val c = [];
1.137 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.138 @@ -432,7 +432,7 @@
1.139
1.140 "----- d2_pqformula10_neg ------";
1.141 val fmz = ["equality (4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.142 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.143 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.144 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.145 (*val p = e_pos'; val c = [];
1.146 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.147 @@ -452,7 +452,7 @@
1.148
1.149 "----- d2_pqformula10 ------";
1.150 val fmz = ["equality (-4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.151 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.152 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.153 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.154 (*val p = e_pos'; val c = [];
1.155 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.156 @@ -471,7 +471,7 @@
1.157
1.158 "----- d2_pqformula9_neg ------";
1.159 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.160 -val (dI',pI',mI') = ("PolyEq.thy",["pqFormula","degree_2","polynomial","univariate","equation"],
1.161 +val (dI',pI',mI') = ("PolyEq",["pqFormula","degree_2","polynomial","univariate","equation"],
1.162 ["PolyEq","solve_d2_polyeq_pq_equation"]);
1.163 (*val p = e_pos'; val c = [];
1.164 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.165 @@ -493,7 +493,7 @@
1.166 "-------------------- test thm's d2_abc_formulsxx[_neg]-----";
1.167
1.168 val fmz = ["equality (-1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.169 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.170 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.171 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.172 (*val p = e_pos'; val c = [];
1.173 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.174 @@ -511,7 +511,7 @@
1.175 | _ => raise error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
1.176
1.177 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.178 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.179 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.180 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.181 (*val p = e_pos'; val c = [];
1.182 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.183 @@ -530,7 +530,7 @@
1.184
1.185 (*EP-11*)
1.186 val fmz = ["equality (-1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.187 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.188 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.189 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.190 (*val p = e_pos'; val c = [];
1.191 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.192 @@ -548,7 +548,7 @@
1.193 | _ => raise error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
1.194
1.195 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.196 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.197 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.198 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.199 (*val p = e_pos'; val c = [];
1.200 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.201 @@ -567,7 +567,7 @@
1.202 "TODO 1 + x + 2*x^^^2 = 0";
1.203
1.204 val fmz = ["equality (-2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.205 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.206 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.207 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.208 (*val p = e_pos'; val c = [];
1.209 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.210 @@ -585,7 +585,7 @@
1.211 | _ => raise error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
1.212
1.213 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.214 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.215 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.216 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.217 (*val p = e_pos'; val c = [];
1.218 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.219 @@ -605,7 +605,7 @@
1.220
1.221 (*EP-12*)
1.222 val fmz = ["equality (-2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.223 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.224 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.225 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.226 (*val p = e_pos'; val c = [];
1.227 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.228 @@ -623,7 +623,7 @@
1.229 | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
1.230
1.231 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.232 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.233 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.234 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.235 (*val p = e_pos'; val c = [];
1.236 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.237 @@ -643,7 +643,7 @@
1.238
1.239 (*EP-13*)
1.240 val fmz = ["equality (-8 + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.241 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.242 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.243 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.244 (*val p = e_pos'; val c = [];
1.245 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.246 @@ -661,7 +661,7 @@
1.247 | _ => raise error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
1.248
1.249 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.250 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.251 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.252 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.253 (*val p = e_pos'; val c = [];
1.254 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.255 @@ -680,7 +680,7 @@
1.256
1.257 (*EP-14*)
1.258 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.259 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.260 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.261 (*val p = e_pos'; val c = [];
1.262 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.263 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.264 @@ -698,7 +698,7 @@
1.265
1.266
1.267 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
1.268 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.269 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"], ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.270 (*val p = e_pos'; val c = [];
1.271 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.272 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
1.273 @@ -716,7 +716,7 @@
1.274
1.275 (*EP-15*)
1.276 val fmz = ["equality (2*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.277 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.278 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.279 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.280 (*val p = e_pos'; val c = [];
1.281 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.282 @@ -734,7 +734,7 @@
1.283 | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.284
1.285 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.286 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.287 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.288 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.289 (*val p = e_pos'; val c = [];
1.290 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.291 @@ -753,7 +753,7 @@
1.292
1.293 (*EP-16*)
1.294 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.295 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.296 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.297 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.298 (*val p = e_pos'; val c = [];
1.299 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.300 @@ -772,7 +772,7 @@
1.301
1.302 (*EP-//*)
1.303 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
1.304 -val (dI',pI',mI') = ("PolyEq.thy",["abcFormula","degree_2","polynomial","univariate","equation"],
1.305 +val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.306 ["PolyEq","solve_d2_polyeq_abc_equation"]);
1.307 (*val p = e_pos'; val c = [];
1.308 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.309 @@ -795,7 +795,7 @@
1.310 val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
1.311 "solveFor x","solutions L"];
1.312 val (dI',pI',mI') =
1.313 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.314 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.315 ["PolyEq","complete_square"]);
1.316 (* val p = e_pos'; val c = [];
1.317 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.318 @@ -806,7 +806,7 @@
1.319 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.320 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.321 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.322 - (*Apply_Method ("PolyEq.thy","complete_square")*)
1.323 + (*Apply_Method ("PolyEq","complete_square")*)
1.324 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.325 (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
1.326 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.327 @@ -854,7 +854,7 @@
1.328 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
1.329 "solveFor x","solutions L"];
1.330 val (dI',pI',mI') =
1.331 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.332 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.333 ["PolyEq","complete_square"]);
1.334 (* val p = e_pos'; val c = [];
1.335 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.336 @@ -868,7 +868,7 @@
1.337 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.338 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.339 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.340 - (*Apply_Method ("PolyEq.thy","complete_square")*)
1.341 + (*Apply_Method ("PolyEq","complete_square")*)
1.342 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.343
1.344 "----------- (-16 + 4*x + 2*x^^^2 = 0), --------------------------";
1.345 @@ -877,7 +877,7 @@
1.346 val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
1.347 "solveFor x","solutions L"];
1.348 val (dI',pI',mI') =
1.349 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.350 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.351 ["PolyEq","complete_square"]);
1.352 (* val p = e_pos'; val c = [];
1.353 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.354 @@ -891,7 +891,7 @@
1.355 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.356 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.357 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.358 - (*Apply_Method ("PolyEq.thy","complete_square")*)
1.359 + (*Apply_Method ("PolyEq","complete_square")*)
1.360 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.361 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.362 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.363 @@ -913,7 +913,7 @@
1.364 val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",
1.365 "solveFor x","solutions L"];
1.366 val (dI',pI',mI') =
1.367 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.368 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.369 ["PolyEq","complete_square"]);
1.370 (* val p = e_pos'; val c = [];
1.371 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.372 @@ -956,7 +956,7 @@
1.373 val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
1.374 "solveFor x","solutions L"];
1.375 val (dI',pI',mI') =
1.376 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.377 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.378 ["PolyEq","complete_square"]);
1.379 (* val p = e_pos'; val c = [];
1.380 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.381 @@ -987,7 +987,7 @@
1.382 val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
1.383 "solveFor x","solutions L"];
1.384 val (dI',pI',mI') =
1.385 - ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
1.386 + ("PolyEq",["degree_2","expanded","univariate","equation"],
1.387 ["PolyEq","complete_square"]);
1.388 (* val p = e_pos'; val c = [];
1.389 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.390 @@ -1017,7 +1017,7 @@
1.391 val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
1.392 (* refine fmz ["univariate","equation"];
1.393 *)
1.394 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.395 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.396 (*val p = e_pos';
1.397 val c = [];
1.398 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.399 @@ -1036,7 +1036,7 @@
1.400 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.401 (* val nxt =
1.402 ("Subproblem",
1.403 - Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
1.404 + Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1.405 : string * tac *)
1.406 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.407 (*val nxt =
1.408 @@ -1061,7 +1061,7 @@
1.409 (*is in rlang.sml, too*)
1.410 val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
1.411 "solveFor x","solutions L"];
1.412 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.413 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.414
1.415 (*val p = e_pos'; val c = [];
1.416 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.417 @@ -1082,7 +1082,7 @@
1.418 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.419 (* val nxt =
1.420 ("Subproblem",
1.421 - Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
1.422 + Subproblem ("PolyEq",["polynomial","univariate","equation"]))
1.423 : string * tac*)
1.424 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.425 (*val nxt =
1.426 @@ -1106,7 +1106,7 @@
1.427 val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
1.428 (* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
1.429 (*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
1.430 -val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
1.431 +val (dI',pI',mI') = ("PolyEq",["univariate","equation"],["no_met"]);
1.432 (*val p = e_pos';
1.433 val c = [];
1.434 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.435 @@ -1169,7 +1169,7 @@
1.436 states:=[];
1.437 CalcTree
1.438 [(["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"],
1.439 - ("PolyEq.thy",["univariate","equation"],["no_met"]))];
1.440 + ("PolyEq",["univariate","equation"],["no_met"]))];
1.441 Iterator 1;
1.442 moveActiveRoot 1;
1.443 autoCalculate 1 CompleteCalc;