1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/systest/scriptnew.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,421 @@
1.4 +(* use"../tests/scriptnew.sml";
1.5 + use"tests/scriptnew.sml";
1.6 + *)
1.7 +
1.8 +(*contents*)
1.9 +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
1.10 +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
1.11 +" --- test 11.5.02 Testeq: let e_ =... in [e_] ------------------ ";
1.12 +" _________________ me + nxt_step from script ___________________ ";
1.13 +" _________________ me + sqrt-equ-test: 1.norm_equation ________ ";
1.14 +" _________________ equation with x =(-12)/5, but L ={} ------- ";
1.15 +(*contents*)
1.16 +
1.17 +
1.18 +
1.19 +
1.20 +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
1.21 +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
1.22 +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
1.23 +store_pbt
1.24 + (prep_pbt Test.thy
1.25 + (["tests"],
1.26 + []:(string * string list) list,
1.27 + e_rls, None, []));
1.28 +store_pbt
1.29 + (prep_pbt Test.thy
1.30 + (["met-testterm","tests"],
1.31 + [("#Given" ,["realTestGiven g_"]),
1.32 + ("#Find" ,["realTestFind f_"])
1.33 + ],
1.34 + e_rls, None, []));
1.35 +methods:= overwritel (!methods,
1.36 +[ prep_met (*test for simplification*)
1.37 + (("Test.thy","met-testterm"):metID,
1.38 + [("#Given" ,["realTestGiven g_"]),
1.39 + ("#Find" ,["realTestFind f_"])
1.40 + ],
1.41 + {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
1.42 + asm_rls=[],asm_thm=[]},
1.43 + "Script Testterm (g_::real) = \
1.44 + \Repeat\
1.45 + \ ((Repeat (Rewrite rmult_1 False)) Or\
1.46 + \ (Repeat (Rewrite rmult_0 False)) Or\
1.47 + \ (Repeat (Rewrite radd_0 False))) g_"
1.48 + )]);
1.49 +val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"];
1.50 +val (dI',pI',mI') = ("Test.thy",["met-testterm","tests"],
1.51 + ("Test.thy","met-testterm"));
1.52 +val p = e_pos'; val c = [];
1.53 +val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.54 +val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;
1.55 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.56 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.57 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.58 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.59 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.60 +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","met-testterm"))*)
1.61 +(*----script 111 ------------------------------------------------*)
1.62 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.63 +(*"(#0 + #0) * (#1 * (#1 * a))" nxt= Rewrite ("rmult_1",*)
1.64 +(*----script 222 ------------------------------------------------*)
1.65 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.66 +(*"(#0 + #0) * (#1 * a)" nxt= Rewrite ("rmult_1",*)
1.67 +(*----script 333 ------------------------------------------------*)
1.68 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.69 +(*"(#0 + #0) * a" nxt= Rewrite ("radd_0",*)
1.70 +(*----script 444 ------------------------------------------------*)
1.71 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.72 +(*"#0 * a"*)
1.73 +(*----script 555 ------------------------------------------------*)
1.74 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.75 +(*"#0"*)
1.76 +if p=([4],Res) then ()
1.77 +else raise error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p));
1.78 +(*----script 666 ------------------------------------------------*)
1.79 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.80 +(*"#0"*)
1.81 +if nxt=("End_Proof'",End_Proof') then ()
1.82 +else raise error "new behaviour in 30.4.02 Testterm: End_Proof";
1.83 +
1.84 +
1.85 +
1.86 +
1.87 +
1.88 +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
1.89 +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
1.90 +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
1.91 +store_pbt
1.92 + (prep_pbt Test.thy
1.93 + (["met-testeq","tests"],
1.94 + [("#Given" ,["boolTestGiven e_"]),
1.95 + ("#Find" ,["boolTestFind v_i_"])
1.96 + ],
1.97 + e_rls, None, []));
1.98 +methods:= overwritel (!methods,
1.99 +[
1.100 + prep_met
1.101 + (("Test.thy","testeq1"):metID,
1.102 + [("#Given",["boolTestGiven e_"]),
1.103 + ("#Where" ,[]),
1.104 + ("#Find" ,["boolTestFind v_i_"])
1.105 + ],
1.106 + {rew_ord'="tless_true",rls'=tval_rls,
1.107 + srls=append_rls "testeq1_srls" e_rls
1.108 + [Calc ("Test.contains'_root", eval_contains_root"")],
1.109 + prls=e_rls,calc=[],asm_rls=[],asm_thm=[("square_equation_left","")]},
1.110 + "Script Testeq (e_::bool) = \
1.111 + \(While (contains_root e_) Do \
1.112 + \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
1.113 + \ (Try (Repeat (Rewrite square_equation_left True))) @@ \
1.114 + \ (Try (Repeat (Rewrite radd_0 False)))))\
1.115 + \ e_"
1.116 + )
1.117 +]);
1.118 +
1.119 +val fmz = ["boolTestGiven (0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0)",
1.120 + "boolTestFind v_i_"];
1.121 +val (dI',pI',mI') = ("Test.thy",["met-testeq","tests"],
1.122 + ("Test.thy","testeq1"));
1.123 +val Script sc = (#scr o get_met) ("Test.thy","testeq1");
1.124 +atomt sc;
1.125 +val p = e_pos'; val c = [];
1.126 +val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.127 +val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;
1.128 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.129 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.130 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.131 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.132 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.133 +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testeq1")) *)
1.134 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.135 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.136 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.137 +(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#0 + sqrt a = #0"))
1.138 +val nxt = ("Rewrite",Rewrite ("radd_0","#0 + ?k = ?k"))*)
1.139 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.140 +
1.141 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.142 +(*** No such constant: "Test.contains'_root" *)
1.143 +
1.144 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.145 +if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso
1.146 + nxt=("End_Proof'",End_Proof') then ()
1.147 +else raise error "different behaviour test 9.5.02 Testeq: While Try Repeat @@";
1.148 +
1.149 +
1.150 +
1.151 +
1.152 +" --- test 11.5.02 Testeq: let e_ =... in [e_] --------- ";
1.153 +" --- test 11.5.02 Testeq: let e_ =... in [e_] --------- ";
1.154 +" --- test 11.5.02 Testeq: let e_ =... in [e_] --------- ";
1.155 +methods:= overwritel (!methods,
1.156 +[
1.157 + prep_met
1.158 + (("Test.thy","testlet"):metID,
1.159 + [("#Given",["boolTestGiven e_"]),
1.160 + ("#Where" ,[]),
1.161 + ("#Find" ,["boolTestFind v_i_"])
1.162 + ],
1.163 + {rew_ord'="tless_true",rls'=tval_rls,
1.164 + srls=append_rls "testlet_srls" e_rls
1.165 + [Calc ("Test.contains'_root",eval_contains_root"")],
1.166 + prls=e_rls,calc=[],asm_rls=[],asm_thm=[("square_equation_left","")]},
1.167 + "Script Testeq2 (e_::bool) = \
1.168 + \(let e_ =\
1.169 + \ ((While (contains_root e_) Do \
1.170 + \ (Rewrite square_equation_left True))\
1.171 + \ e_)\
1.172 + \in [e_::bool])"
1.173 + )
1.174 + ]);
1.175 +val Script sc = (#scr o get_met) ("Test.thy","testlet");
1.176 +writeln(term2str sc);
1.177 +val fmz = ["boolTestGiven (sqrt a = 0)",
1.178 + "boolTestFind v_i_"];
1.179 +val (dI',pI',mI') = ("Test.thy",["met-testeq","tests"],
1.180 + ("Test.thy","testlet"));
1.181 +val p = e_pos'; val c = [];
1.182 +val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.183 +val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;
1.184 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.185 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.186 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.187 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.188 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.189 +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testlet"))*)
1.190 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.191 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.192 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.193 +if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso
1.194 + nxt=("End_Proof'",End_Proof') then ()
1.195 +else raise error "different behaviour in test 11.5.02 Testeq: let e_ =... in [e_]";
1.196 +
1.197 +
1.198 +
1.199 +
1.200 +" _________________ me + nxt_step from script _________________ ";
1.201 +" _________________ me + nxt_step from script _________________ ";
1.202 +" _________________ me + nxt_step from script _________________ ";
1.203 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.204 + "solveFor x","errorBound (eps=0)",
1.205 + "solutions L"];
1.206 +val (dI',pI',mI') =
1.207 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.208 + ("Test.thy","sqrt-equ-test"));
1.209 +val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test");
1.210 +writeln(term2str sc);
1.211 +
1.212 +val p = e_pos'; val c = [];
1.213 +"--- s1 ---";
1.214 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.215 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.216 +"--- s2 ---";
1.217 +(* val nxt =
1.218 + ("Add_Given",
1.219 + Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)
1.220 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.221 +"--- s3 ---";
1.222 +(* val nxt = ("Add_Given",Add_Given "solveFor x");*)
1.223 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.224 +"--- s4 ---";
1.225 +(* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)
1.226 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.227 +"--- s5 ---";
1.228 +(* val nxt = ("Add_Find",Add_Find "solutions L");*)
1.229 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.230 +"--- s6 ---";
1.231 +(* val nxt = ("Specify_Domain",Specify_Domain "Test.thy");*)
1.232 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.233 +"--- s7 ---";
1.234 +(* val nxt =
1.235 + ("Specify_Problem",
1.236 + Specify_Problem ["sqroot-test","univariate","equation","test"]);*)
1.237 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.238 +"--- s8 ---";
1.239 +(* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)
1.240 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.241 +"--- s9 ---";
1.242 +(* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)
1.243 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.244 +"--- 1 ---";
1.245 +(* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)
1.246 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.247 +"--- 2 ---";
1.248 +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
1.249 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.250 +"--- 3 ---";
1.251 +(* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)
1.252 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.253 +"--- 4 ---";
1.254 +(* val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");*)
1.255 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.256 +"--- 5 ---";
1.257 +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
1.258 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.259 +"--- 6 ---";
1.260 +(* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)
1.261 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.262 +"--- 7 ---";
1.263 +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
1.264 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.265 +"--- 8<> ---";
1.266 +(* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)
1.267 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.268 +"--- 9<> ---";
1.269 +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
1.270 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.271 +"--- 10<> ---";
1.272 +(* val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");*)
1.273 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.274 +"--- 11<> ---";
1.275 +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
1.276 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.277 +"--- 12<> ---.";
1.278 +(* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));*)
1.279 +get_form nxt p pt;
1.280 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.281 +"--- 13<> ---";
1.282 +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
1.283 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.284 +"--- 14<> ---";
1.285 +(* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*)
1.286 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.287 +if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
1.288 +then raise error "scriptnew.sml 1: me + msteps from script: new behaviour"
1.289 +else ();
1.290 +"--- 15<> ---";
1.291 +(* val nxt = ("End_Proof'",End_Proof');*)
1.292 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.293 +
1.294 +writeln (pr_ptree pr_short pt);
1.295 +writeln("result: "^(get_obj g_result pt [])^
1.296 +"\n=============================================================");
1.297 +(*get_obj g_asm pt [];
1.298 +val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*)
1.299 +
1.300 +
1.301 +
1.302 +
1.303 +
1.304 +" _________________ me + sqrt-equ-test: 1.norm_equation _________________ ";
1.305 +" _________________ me + sqrt-equ-test: 1.norm_equation _________________ ";
1.306 +" _________________ me + sqrt-equ-test: 1.norm_equation _________________ ";
1.307 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
1.308 + "solveFor x","errorBound (eps=0)",
1.309 + "solutions L"];
1.310 +val (dI',pI',mI') =
1.311 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.312 + ("Test.thy","sqrt-equ-test"));
1.313 + val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test");
1.314 + (writeln o term2str) sc;
1.315 +val p = e_pos'; val c = [];
1.316 +"--- s1 ---";
1.317 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.318 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.319 +"--- s2 ---";
1.320 +(* val nxt = ("Add_Given",
1.321 + Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)
1.322 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.323 +"--- s3 ---";
1.324 +(* val nxt = ("Add_Given",Add_Given "solveFor x");*)
1.325 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.326 +"--- s4 ---";
1.327 +(* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)
1.328 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.329 +"--- s5 ---";
1.330 +(* val nxt = ("Add_Find",Add_Find "solutions L");*)
1.331 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.332 +"--- s6 ---";
1.333 +(* val nxt = ("Specify_Domain",Specify_Domain "Test.thy");*)
1.334 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.335 +"--- s7 ---";
1.336 +(* val nxt = ("Specify_Problem",
1.337 + Specify_Problem ["sqroot-test","univariate","equation","test"]);*)
1.338 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.339 +"--- s8 ---";
1.340 +(* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)
1.341 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.342 +"--- s9 ---";
1.343 +(* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)
1.344 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.345 +"--- !!! x1 --- 1.norm_equation";
1.346 +(*###*)val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
1.347 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.348 +"--- !!! x2 --- 1.norm_equation";
1.349 +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
1.350 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.351 +(*(me nxt p [1] pt) handle e => print_exn_G e;*)
1.352 +"--- !!! x3 --- 1.norm_equation";
1.353 +(*val nxt = ("Empty_Mstep",Empty_Mstep) ### helpless*)
1.354 +(*###*)val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
1.355 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.356 +"--- !!! x4 --- 1.norm_equation";
1.357 +(*val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root")*)
1.358 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.359 +"--- !!! x5 --- 1.norm_equation";
1.360 +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
1.361 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.362 +if f= Form'(FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"))
1.363 +then() else raise error "new behaviour in test-example 1.norm sqrt-equ-test";
1.364 +
1.365 +
1.366 +(* use"../tests/scriptnew.sml";
1.367 + *)
1.368 +
1.369 +" _________________ equation with x =(-12)/5, but L ={} ------- ";
1.370 +
1.371 +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",
1.372 + "solveFor x","errorBound (eps=0)",
1.373 + "solutions L"];
1.374 +val (dI',pI',mI') =
1.375 + ("Test.thy",["sqroot-test","univariate","equation","test"],
1.376 + ("Test.thy","square_equation"));
1.377 +val p = e_pos'; val c = [];
1.378 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
1.379 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
1.380 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.381 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.382 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.383 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.384 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.385 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.386 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.387 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.388 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.389 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.390 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.391 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.392 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.393 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.394 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.395 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.396 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.397 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.398 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.399 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.400 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.401 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.402 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.403 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.404 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.405 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.406 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.407 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.408 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.409 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.410 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.411 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.412 +trace_rewrite:=true;
1.413 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.414 +
1.415 +trace_rewrite:=false;
1.416 +
1.417 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.418 +val Form' (FormKF (_,_,_,_,ff)) = f;
1.419 +if ff="[]" then ()
1.420 +else raise error "diff.behav. in scriptnew.sml; root-eq: L = []";
1.421 +
1.422 +
1.423 +val tt = (term_of o the o (parse thy)) "?xxx";
1.424 +rewrite_set_ thy true tval_rls ;