1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/FE-KE.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,403 @@
1.4 +(* use"test-FE-KE.sml";
1.5 + W.N.16.4.00
1.6 + *)
1.7 +
1.8 +(*contents*)
1.9 +" _________________ stdin: tutor active_________________ ";
1.10 +" _________________ stdin: student active_________________ ";
1.11 +" _________________ stdin: root_equ: 1.norm_equation ________________ ";
1.12 +" _________________ stdin: root_equ: spec_hide ________________ ";
1.13 +" ------------- test-FE-KE.sml: test100 ------------- ";
1.14 +" _________________ stdin: root_equ: Auto ________________ ";
1.15 +(*contents*)
1.16 +
1.17 +
1.18 +
1.19 +
1.20 +(*#########################################################*)
1.21 +" _________________ stdin: tutor active_________________ ";
1.22 +" _________________ stdin: tutor active_________________ ";
1.23 +" _________________ stdin: tutor active_________________ ";
1.24 +" _________________ stdin: tutor active_________________ ";
1.25 +" _________________ stdin: tutor active_________________ ";
1.26 +" _________________ stdin: tutor active_________________ ";
1.27 +proofs:= []; dials:=([],[],[]);
1.28 +StdinSML 0 0 0 0 New_User;
1.29 +set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*)
1.30 +StdinSML 1 0 0 0 New_Proof;
1.31 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.32 + "solveFor x","errorBound (eps=0)",
1.33 + "solutions L"];
1.34 +val (dI',pI',mI') =
1.35 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.36 + ("Test.thy","sqrt-equ-test"));
1.37 +"--- s1 ---";
1.38 +val (_,1,1,1,[],[_,_,PpcKF (_,_,_,_,ppc),req],_) =
1.39 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.40 +"--- s2 ---";
1.41 +StdinSML 1 1 ~1 ~1 (Command Accept);
1.42 +(*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*)
1.43 +"--- s3 ---";
1.44 +StdinSML 1 1 ~2 ~2 (Command Accept);
1.45 +(*RuleFK (Add_Given "solveFor x")*)
1.46 +"--- s4 ---";
1.47 +StdinSML 1 1 ~3 ~3 (Command Accept);
1.48 +(*RuleFK (Add_Given "errorBound (eps = #0)")*)
1.49 +"--- s5 ---";
1.50 +StdinSML 1 1 ~4 ~4 (Command Accept);
1.51 +(*RuleFK (Add_Find "solutions L")*)
1.52 +"--- s6 ---";
1.53 +StdinSML 1 1 ~5 ~5 (Command Accept);
1.54 +(*RuleFK (Specify_Domain "Test.thy")*)
1.55 +"--- s7 ---";
1.56 +StdinSML 1 1 ~6 ~6 (Command Accept);
1.57 +(*RuleFK (Specify_Problem ["sqroot-test","univariate","equation","test"])*)
1.58 +"--- s8 ---";
1.59 +StdinSML 1 1 ~7 ~7 (Command Accept);
1.60 +(*RuleFK (Specify_Method ("Test.thy","sqrt-equ-test"))*)
1.61 +"--- s9 ---";
1.62 +val (_,1,1,~8,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.63 +StdinSML 1 1 ~8 ~8 (Command Accept);
1.64 +if ct'="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)" andalso
1.65 +r = Apply_Method ("Test.thy","sqrt-equ-test")
1.66 +then () else raise error "new behaviour in test-example";
1.67 +(*RuleFK (Apply_Method ("Test.thy","sqrt-equ-test"))*)
1.68 +
1.69 +"--- 1 ---";
1.70 +val (_,1,1,~9,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.71 +StdinSML 1 1 ~9 ~9 (Command Accept);
1.72 +(*RuleFK (Rewrite ("square_equation_left",""))*)
1.73 +"--- 2 ---";
1.74 +val (_,1,1,~10,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.75 +StdinSML 1 1 ~10 ~10 (Command Accept);
1.76 +(*RuleFK (Rewrite_Set "Test_simplify")*)
1.77 +"--- 3 ---";
1.78 +val (_,1,1,~11,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.79 +StdinSML 1 1 ~11 ~11 (Command Accept);
1.80 +(*RuleFK (Rewrite_Set "rearrange_assoc")*)
1.81 +"--- 4 ---";
1.82 +val (_,1,1,~12,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.83 +StdinSML 1 1 ~12 ~12 (Command Accept);
1.84 +(*RuleFK (Rewrite_Set "isolate_root")*)
1.85 +"--- 5 ---";
1.86 +val (_,1,1,~13,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.87 +StdinSML 1 1 ~13 ~13 (Command Accept);
1.88 +(*RuleFK (Rewrite_Set "Test_simplify")*)
1.89 +"--- 6 ---";
1.90 +val (_,1,1,~14,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.91 +StdinSML 1 1 ~14 ~14 (Command Accept);
1.92 +(*RuleFK (Rewrite ("square_equation_left",""))*)
1.93 +"--- 7 ---";
1.94 +val (_,1,1,~15,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.95 +StdinSML 1 1 ~15 ~15 (Command Accept);
1.96 +(*RuleFK (Rewrite_Set "Test_simplify")*)
1.97 +"--- 8 ---";
1.98 +val (_,1,1,~16,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.99 +StdinSML 1 1 ~16 ~16 (Command Accept);
1.100 +(*val r = Rewrite_Set "rearrange_assoc"*)
1.101 +"--- 9 ---";
1.102 +val (_,1,1,~17,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.103 +StdinSML 1 1 ~17 ~17 (Command Accept);
1.104 +(*RuleFK (Rewrite_Set "Test_simplify")*)
1.105 +"--- 10 ---";
1.106 +val (_,1,1,~18,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.107 +StdinSML 1 1 ~18 ~18 (Command Accept);
1.108 +(*val r = Rewrite_Set "norm_equation"*)
1.109 +"--- 11 ---";
1.110 +val (_,1,1,~19,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.111 +StdinSML 1 1 ~19 ~19 (Command Accept);
1.112 +(*RuleFK (Rewrite_Set "Test_simplify")*)
1.113 +"--- 13 ---";
1.114 +val (_,1,1,~20,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.115 +StdinSML 1 1 ~20 ~20 (Command Accept);
1.116 +(*RuleFK (Rewrite_Set_Inst ([(#,#)],"isolate_bdv"))*)
1.117 +"--- 14 ---";
1.118 +val (_,1,1,~21,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.119 +StdinSML 1 1 ~21 ~21 (Command Accept);
1.120 +(*RuleFK (Rewrite_Set "Test_simplify")*)
1.121 +"--- 15 ---";
1.122 +val (_,1,1,~22,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) =
1.123 +StdinSML 1 1 ~22 ~22 (Command Accept);
1.124 +"--- 16 ---";
1.125 +val (_,1,1,~23,[],[req,End_Proof],_) =
1.126 +StdinSML 1 1 ~23 ~23 (Command Accept);
1.127 +
1.128 +(*
1.129 +"=====================";=======================
1.130 + use"test-FE-KE.sml";
1.131 + *)
1.132 +
1.133 +
1.134 +(*#########################################################*)
1.135 +" _________________ stdin: student active_________________ ";
1.136 +" _________________ stdin: student active_________________ ";
1.137 +" _________________ stdin: student active_________________ ";
1.138 +" _________________ stdin: student active_________________ ";
1.139 +" _________________ stdin: student active_________________ ";
1.140 +" _________________ stdin: student active_________________ ";
1.141 +proofs:= []; dials:=([],[],[]);
1.142 +StdinSML 0 0 0 0 New_User;
1.143 +set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*)
1.144 +(*SelRule WORKS BY CAHCNE, and wrong, IN SPECIFY*)
1.145 +StdinSML 1 0 0 0 New_Proof;
1.146 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.147 + "solveFor x","errorBound (eps=0)",
1.148 + "solutions L"];
1.149 +val (dI',pI',mI') =
1.150 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.151 + ("Test.thy","sqrt-equ-test"));
1.152 +"--- s1 ---";
1.153 +val (_,1,1,1,[],[_,_,PpcKF (_,_,_,_,f), Select _, req],_) =
1.154 + StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.155 +"--- s2 ---";
1.156 +(*val (_,1,1,~1,[],[PpcKF (_,_,_,_,ppc),RuleKF (_,r),req],_) = *)
1.157 + StdinSML 1 1 ~1 ~1
1.158 + (RuleFK (Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"));
1.159 +"--- s3 ---";
1.160 +StdinSML 1 1 ~2 ~2 (RuleFK (Add_Given "solveFor x"));
1.161 +"--- s4 ---";
1.162 +StdinSML 1 1 ~3 ~3 (RuleFK (Add_Given "errorBound (eps = 0)"));
1.163 +"--- s5 ---";
1.164 +StdinSML 1 1 ~4 ~4 (RuleFK (Add_Find "solutions L"));
1.165 +"--- s6 ---";
1.166 +StdinSML 1 1 ~5 ~5 (RuleFK (Specify_Domain "Test.thy"));
1.167 +"--- s7 ---";
1.168 +StdinSML 1 1 ~6 ~6 (RuleFK
1.169 +(Specify_Problem ["sqroot-test","univariate","equation","test"]));
1.170 +"--- s8 ---";
1.171 +StdinSML 1 1 ~7 ~7 (RuleFK (Specify_Method ("Test.thy","sqrt-equ-test")));
1.172 +"--- s9 ---";
1.173 +StdinSML 1 1 ~8 ~8 (RuleFK (Apply_Method ("Test.thy","sqrt-equ-test")));
1.174 +"--- 1 ---";
1.175 +StdinSML 1 1 ~9 ~9 (RuleFK (Rewrite ("square_equation_left","")));
1.176 +"--- 2 ---";
1.177 +StdinSML 1 1 ~10 ~10 (RuleFK (Rewrite_Set "Test_simplify"));
1.178 +"--- 3 ---";
1.179 +StdinSML 1 1 ~11 ~11 (RuleFK (Rewrite_Set "rearrange_assoc"));
1.180 +"--- 4 ---";
1.181 +StdinSML 1 1 ~12 ~12 (RuleFK (Rewrite_Set "isolate_root"));
1.182 +"--- 5 ---";
1.183 +StdinSML 1 1 ~13 ~13 (RuleFK (Rewrite_Set "Test_simplify"));
1.184 +"--- 6 ---";
1.185 +StdinSML 1 1 ~14 ~14 (RuleFK
1.186 +(Rewrite ("square_equation_left","")));
1.187 +"--- 7 ---";
1.188 +StdinSML 1 1 ~15 ~15 (RuleFK (Rewrite_Set "Test_simplify"));
1.189 +"--- 8<> ---";
1.190 +StdinSML 1 1 ~16 ~16 (RuleFK (Rewrite_Set "rearrange_assoc"));
1.191 +"--- 9<> ---";
1.192 +StdinSML 1 1 ~17 ~17 (RuleFK (Rewrite_Set "Test_simplify"));
1.193 +"--- 10<> ---";
1.194 +StdinSML 1 1 ~18 ~18 (RuleFK (Rewrite_Set "norm_equation"));
1.195 +"--- 11<> ---";
1.196 +StdinSML 1 1 ~19 ~19 (RuleFK (Rewrite_Set "Test_simplify"));
1.197 +"--- 12<> ---";
1.198 +StdinSML 1 1 ~20 ~20 (RuleFK
1.199 +(Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")));
1.200 +"--- 13<> ---";
1.201 +StdinSML 1 1 ~21 ~21 (RuleFK (Rewrite_Set "Test_simplify"));
1.202 +"--- 14<> ---";
1.203 +val (begin,uI,pI,acI,cI,dats,eend) =
1.204 +StdinSML 1 1 ~22 ~22 (RuleFK
1.205 +(Check_Postcond ["sqroot-test","univariate","equation","test"]));
1.206 +
1.207 +
1.208 +(*
1.209 +"=====================";=======================
1.210 + use"test-FE-KE.sml";
1.211 + *)
1.212 +
1.213 +
1.214 +
1.215 +
1.216 +" _________________ stdin: root_equ: 1.norm_equation ________________ ";
1.217 +" _________________ stdin: root_equ: 1.norm_equation ________________ ";
1.218 +" _________________ stdin: root_equ: 1.norm_equation ________________ ";
1.219 +" _________________ stdin: root_equ: 1.norm_equation ________________ ";
1.220 +" _________________ stdin: root_equ: 1.norm_equation ________________ ";
1.221 +" _________________ stdin: root_equ: 1.norm_equation ________________ ";
1.222 +proofs:= []; dials:=([],[],[]);
1.223 +StdinSML 0 0 0 0 New_User;
1.224 +set_dstate 1 test_hide 0 2;
1.225 +StdinSML 1 0 0 0 New_Proof;
1.226 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.227 + "solveFor x","errorBound (eps=0)",
1.228 + "solutions L"];
1.229 +val (dI',pI',mI') =
1.230 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.231 + ("Test.thy","sqrt-equ-test"));
1.232 +"--- s1 ---";
1.233 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.234 +"--- s2 ---";
1.235 +StdinSML 1 1 ~1 ~1 (Command Accept);
1.236 +(*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*)
1.237 +"--- s3 ---";
1.238 +StdinSML 1 1 ~2 ~2 (Command Accept);
1.239 +(*RuleFK (Add_Given "solveFor x")*)
1.240 +"--- s4 ---";
1.241 +StdinSML 1 1 ~3 ~3 (Command Accept);
1.242 +(*RuleFK (Add_Given "errorBound (eps = #0)")*)
1.243 +"--- s5 ---";
1.244 +StdinSML 1 1 ~4 ~4 (Command Accept);
1.245 +(*RuleFK (Add_Find "solutions L")*)
1.246 +"--- s6 ---";
1.247 +StdinSML 1 1 ~5 ~5 (Command Accept);
1.248 +(*RuleFK (Specify_Domain "Test.thy")*)
1.249 +"--- s7 ---";
1.250 +StdinSML 1 1 ~6 ~6 (Command Accept);
1.251 +(*RuleFK (Specify_Problem ["sqroot-test","univariate","equation","test"])*)
1.252 +"--- s8 ---";
1.253 +StdinSML 1 1 ~7 ~7 (Command Accept);
1.254 +(*RuleFK (Specify_Method ("Test.thy","sqrt-equ-test"))*)
1.255 +"--- s9 ---";
1.256 +val (_,1,1,~8,[],[RuleKF (_,r),FormKF (_,_,_,_,f),req],_) =
1.257 +StdinSML 1 1 ~8 ~8 (Command Accept);
1.258 +(*RuleFK (Apply_Method ("Test.thy","sqrt-equ-test"))*)
1.259 +"--- !!! x1 --- strange choice";
1.260 +StdinSML 1 1 ~9 2 (RuleFK (Rewrite_Set "norm_equation"));
1.261 +"--- !!! x2 --- ME knows nxt_step";
1.262 +StdinSML 1 1 ~10 3 (RuleFK (Rewrite_Set "Test_simplify"));
1.263 +"--- !!! x3 --- helpless !!!";
1.264 +StdinSML 1 1 ~11 4 (RuleFK (Rewrite_Set "rearrange_assoc"));
1.265 +"--- !!! x4 ---";
1.266 +StdinSML 1 1 ~12 5 (RuleFK (Rewrite_Set "isolate_root"));
1.267 +"--- !!! x5 --- back at original equation !!!";
1.268 +val (_,_,_,_,_,[FormKF (_,_,_,_,res),requ],_) =
1.269 +StdinSML 1 1 ~13 5 (RuleFK (Rewrite_Set "Test_simplify"));
1.270 +if res="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"
1.271 +then () else raise error "new behaviour in 1.norm_equ";
1.272 +
1.273 +(*
1.274 +"=====================================";=====@@@@@s=====
1.275 + use"test-FE-KE.sml";
1.276 + W.N.16.4.00
1.277 + *)
1.278 +
1.279 +" _________________ stdin: root_equ: spec_hide ________________ ";
1.280 +" _________________ stdin: root_equ: spec_hide ________________ ";
1.281 +" _________________ stdin: root_equ: spec_hide ________________ ";
1.282 +" _________________ stdin: root_equ: spec_hide ________________ ";
1.283 +" _________________ stdin: root_equ: spec_hide ________________ ";
1.284 +" _________________ stdin: root_equ: spec_hide ________________ ";
1.285 +" _________________ stdin: root_equ: spec_hide ________________ ";
1.286 +proofs:= []; dials:=([],[],[]);
1.287 +StdinSML 0 0 0 0 New_User;
1.288 +set_dstate 1 spec_hide 4 1;
1.289 +StdinSML 1 0 0 0 New_Proof;
1.290 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.291 + "solveFor x","errorBound (eps=0)",
1.292 + "solutions L"];
1.293 +val (dI',pI',mI') =
1.294 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.295 + ("Test.thy","sqrt-equ-test"));
1.296 +val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test");
1.297 +writeln(term2str sc);
1.298 +"--- s1 ---";
1.299 +val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),Select _,req],_) =
1.300 +
1.301 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.302 +"--- !!! x1 --- strange choice"; (*TODO 31.10.00: hier nochmals spec ?!?!?*)
1.303 +StdinSML 1 1 ~1 ~1 (RuleFK (Rewrite_Set "norm_equation"));
1.304 +"--- !!! x2 --- ME knows nxt_step";
1.305 +StdinSML 1 1 ~2 ~2 (RuleFK (Rewrite_Set "Test_simplify"));
1.306 +"--- !!! x3 --- helpless !!!";
1.307 +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) =
1.308 +StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Set "rearrange_assoc"));
1.309 +"--- !!! x4 ---";
1.310 +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) =
1.311 +StdinSML 1 1 ~4 ~4 (RuleFK (Rewrite_Set "isolate_root"));
1.312 +"--- !!! x5 --- back at original equation !!!";
1.313 +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) =
1.314 +
1.315 +StdinSML 1 1 ~5 ~5 (RuleFK (Rewrite_Set "Test_simplify"));
1.316 +if res="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"
1.317 +then () else raise error "new behaviour in test-example";
1.318 +
1.319 +"--- !!! x6 --- not applicable";
1.320 +val (_,_,_,_,_,[Error_ err,Select _,requ],_) =
1.321 +StdinSML 1 1 ~6 ~6 (RuleFK (Rewrite_Set "Test_simplify"));
1.322 +
1.323 +val (_,_,_,_,_,[RuleKF r,FormKF (_,_,_,_,f),requ],_) =
1.324 +StdinSML 1 1 ~6 ~6 (Command YourTurn);
1.325 +
1.326 +StdinSML 1 1 ~7 ~7 (Command ActiveMinus);
1.327 +StdinSML 1 1 ~7 ~7 (Command ActiveMinus);
1.328 +StdinSML 1 1 ~7 ~7 (Command ActiveMinus);
1.329 +StdinSML 1 1 ~7 ~7 (Command ActiveMinus);(*acti=0*)
1.330 +StdinSML 1 1 ~7 ~7 (Command SpeedPlus);(*speed=2:PutRule,TskipS..PutRuleRes,Tt.*)
1.331 +StdinSML 1 1 ~7 ~7 (Command Accept);
1.332 +StdinSML 1 1 ~8 ~8 (Command Accept);
1.333 +StdinSML 1 1 ~9 ~9 (Command Accept);
1.334 +StdinSML 1 1 ~10 ~10 (Command Accept);
1.335 +StdinSML 1 1 ~11 ~11 (Command Accept);
1.336 +StdinSML 1 1 ~12 ~12 (Command Accept);
1.337 +StdinSML 1 1 ~13 ~13 (Command Accept);
1.338 +StdinSML 1 1 ~14 ~14 (Command Accept);
1.339 +
1.340 +(*17.9.02: nach Umbau KB wird Equ immer gr"osser ?!-----
1.341 +StdinSML 1 1 ~15 ~15 (Command Accept);
1.342 +StdinSML 1 1 ~16 ~16 (Command Accept);
1.343 +StdinSML 1 1 ~17 ~17 (Command Accept);
1.344 +StdinSML 1 1 ~18 ~18 (Command Accept);
1.345 +val (_,1,1,_,_,[FormKF (~20,_,0,_,f),req],_) =
1.346 +StdinSML 1 1 ~19 ~19 (Command Accept);
1.347 +if f="[x = 4]" then () else raise error "new behaviour in test-example";
1.348 +
1.349 +val (_,1,1,~20,[],[Request "start another example",End_Proof],_) =
1.350 +StdinSML 1 1 ~20 ~20 (Command Accept);
1.351 +--------------------------------------------------------------------*)
1.352 +
1.353 +(*
1.354 +"=====================================";=====@@@@@=====
1.355 + use"test-FE-KE.sml";
1.356 + *)
1.357 +
1.358 +
1.359 +" ------------- test-FE-KE.sml: test100 ------------- ";
1.360 +" ------------- test-FE-KE.sml: test100 ------------- ";
1.361 +" ------------- test-FE-KE.sml: test100 ------------- ";
1.362 +" ------------- test-FE-KE.sml: test100 ------------- ";
1.363 +" ------------- test-FE-KE.sml: test100 ------------- ";
1.364 +" ------------- test-FE-KE.sml: test100 ------------- ";
1.365 +StdinSML 0 0 0 0 New_User;
1.366 +StdinSML 1 0 0 0 New_Proof;
1.367 +val fmz = ["realTestGiven (0+0)*(1*(1*a))",
1.368 + "realTestFind a"];
1.369 +val (dI',pI',mI') =
1.370 + ("Script.thy",["Script.thy","pbl-testterm"],
1.371 + ("Script.thy","met-testterm"));
1.372 +"--- s1 ---";
1.373 +(*
1.374 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.375 +*** Type unification failed: Clash of types "Descript.una" and "RealDef.real".
1.376 +*)
1.377 +"--- s2 ---";
1.378 +(*too many problems with setup of this example*)
1.379 +
1.380 +
1.381 +" _________________ stdin: root_equ: Auto ________________ ";
1.382 +" _________________ stdin: root_equ: Auto ________________ ";
1.383 +" _________________ stdin: root_equ: Auto ________________ ";
1.384 +" _________________ stdin: root_equ: Auto ________________ ";
1.385 +" _________________ stdin: root_equ: Auto ________________ ";
1.386 +proofs:= []; dials:=([],[],[]);
1.387 +StdinSML 0 0 0 0 New_User;
1.388 +set_dstate 1 spec_hide 4 1;
1.389 +StdinSML 1 0 0 0 New_Proof;
1.390 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.391 + "solveFor x","errorBound (eps=0)",
1.392 + "solutions L"];
1.393 +val (dI',pI',mI') =
1.394 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.395 + ("Test.thy","sqrt-equ-test"));
1.396 +"--- s1 ---";
1.397 +val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),Select _,req],_) =
1.398 +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI'))));
1.399 +
1.400 +val (_,1,1,~1,[],
1.401 + [RuleKF _,_,_,_,_,_,_,_,_,_,_,_,_,_,_,req,End_Proof],_) =
1.402 +StdinSML 1 1 ~1 ~1 (Command Auto);
1.403 +
1.404 +
1.405 +
1.406 +"######################### test-FE_KE.sml complete #####################";