|
1 (* use"../tests/scriptnew.sml"; |
|
2 use"tests/scriptnew.sml"; |
|
3 *) |
|
4 |
|
5 (*contents*) |
|
6 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; |
|
7 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; |
|
8 " --- test 11.5.02 Testeq: let e_ =... in [e_] ------------------ "; |
|
9 " _________________ me + nxt_step from script ___________________ "; |
|
10 " _________________ me + sqrt-equ-test: 1.norm_equation ________ "; |
|
11 " _________________ equation with x =(-12)/5, but L ={} ------- "; |
|
12 (*contents*) |
|
13 |
|
14 |
|
15 |
|
16 |
|
17 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; |
|
18 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; |
|
19 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; |
|
20 store_pbt |
|
21 (prep_pbt Test.thy |
|
22 (["tests"], |
|
23 []:(string * string list) list, |
|
24 e_rls, None, [])); |
|
25 store_pbt |
|
26 (prep_pbt Test.thy |
|
27 (["met-testterm","tests"], |
|
28 [("#Given" ,["realTestGiven g_"]), |
|
29 ("#Find" ,["realTestFind f_"]) |
|
30 ], |
|
31 e_rls, None, [])); |
|
32 methods:= overwritel (!methods, |
|
33 [ prep_met (*test for simplification*) |
|
34 (("Test.thy","met-testterm"):metID, |
|
35 [("#Given" ,["realTestGiven g_"]), |
|
36 ("#Find" ,["realTestFind f_"]) |
|
37 ], |
|
38 {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], |
|
39 asm_rls=[],asm_thm=[]}, |
|
40 "Script Testterm (g_::real) = \ |
|
41 \Repeat\ |
|
42 \ ((Repeat (Rewrite rmult_1 False)) Or\ |
|
43 \ (Repeat (Rewrite rmult_0 False)) Or\ |
|
44 \ (Repeat (Rewrite radd_0 False))) g_" |
|
45 )]); |
|
46 val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"]; |
|
47 val (dI',pI',mI') = ("Test.thy",["met-testterm","tests"], |
|
48 ("Test.thy","met-testterm")); |
|
49 val p = e_pos'; val c = []; |
|
50 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
51 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree; |
|
52 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
53 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
54 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
55 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
56 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
57 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","met-testterm"))*) |
|
58 (*----script 111 ------------------------------------------------*) |
|
59 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
60 (*"(#0 + #0) * (#1 * (#1 * a))" nxt= Rewrite ("rmult_1",*) |
|
61 (*----script 222 ------------------------------------------------*) |
|
62 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
63 (*"(#0 + #0) * (#1 * a)" nxt= Rewrite ("rmult_1",*) |
|
64 (*----script 333 ------------------------------------------------*) |
|
65 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
66 (*"(#0 + #0) * a" nxt= Rewrite ("radd_0",*) |
|
67 (*----script 444 ------------------------------------------------*) |
|
68 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
69 (*"#0 * a"*) |
|
70 (*----script 555 ------------------------------------------------*) |
|
71 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
72 (*"#0"*) |
|
73 if p=([4],Res) then () |
|
74 else raise error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p)); |
|
75 (*----script 666 ------------------------------------------------*) |
|
76 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
77 (*"#0"*) |
|
78 if nxt=("End_Proof'",End_Proof') then () |
|
79 else raise error "new behaviour in 30.4.02 Testterm: End_Proof"; |
|
80 |
|
81 |
|
82 |
|
83 |
|
84 |
|
85 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; |
|
86 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; |
|
87 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; |
|
88 store_pbt |
|
89 (prep_pbt Test.thy |
|
90 (["met-testeq","tests"], |
|
91 [("#Given" ,["boolTestGiven e_"]), |
|
92 ("#Find" ,["boolTestFind v_i_"]) |
|
93 ], |
|
94 e_rls, None, [])); |
|
95 methods:= overwritel (!methods, |
|
96 [ |
|
97 prep_met |
|
98 (("Test.thy","testeq1"):metID, |
|
99 [("#Given",["boolTestGiven e_"]), |
|
100 ("#Where" ,[]), |
|
101 ("#Find" ,["boolTestFind v_i_"]) |
|
102 ], |
|
103 {rew_ord'="tless_true",rls'=tval_rls, |
|
104 srls=append_rls "testeq1_srls" e_rls |
|
105 [Calc ("Test.contains'_root", eval_contains_root"")], |
|
106 prls=e_rls,calc=[],asm_rls=[],asm_thm=[("square_equation_left","")]}, |
|
107 "Script Testeq (e_::bool) = \ |
|
108 \(While (contains_root e_) Do \ |
|
109 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ |
|
110 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ |
|
111 \ (Try (Repeat (Rewrite radd_0 False)))))\ |
|
112 \ e_" |
|
113 ) |
|
114 ]); |
|
115 |
|
116 val fmz = ["boolTestGiven (0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0)", |
|
117 "boolTestFind v_i_"]; |
|
118 val (dI',pI',mI') = ("Test.thy",["met-testeq","tests"], |
|
119 ("Test.thy","testeq1")); |
|
120 val Script sc = (#scr o get_met) ("Test.thy","testeq1"); |
|
121 atomt sc; |
|
122 val p = e_pos'; val c = []; |
|
123 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
124 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree; |
|
125 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
126 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
127 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
128 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
129 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
130 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testeq1")) *) |
|
131 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
132 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
133 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
134 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#0 + sqrt a = #0")) |
|
135 val nxt = ("Rewrite",Rewrite ("radd_0","#0 + ?k = ?k"))*) |
|
136 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
137 |
|
138 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
139 (*** No such constant: "Test.contains'_root" *) |
|
140 |
|
141 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
142 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso |
|
143 nxt=("End_Proof'",End_Proof') then () |
|
144 else raise error "different behaviour test 9.5.02 Testeq: While Try Repeat @@"; |
|
145 |
|
146 |
|
147 |
|
148 |
|
149 " --- test 11.5.02 Testeq: let e_ =... in [e_] --------- "; |
|
150 " --- test 11.5.02 Testeq: let e_ =... in [e_] --------- "; |
|
151 " --- test 11.5.02 Testeq: let e_ =... in [e_] --------- "; |
|
152 methods:= overwritel (!methods, |
|
153 [ |
|
154 prep_met |
|
155 (("Test.thy","testlet"):metID, |
|
156 [("#Given",["boolTestGiven e_"]), |
|
157 ("#Where" ,[]), |
|
158 ("#Find" ,["boolTestFind v_i_"]) |
|
159 ], |
|
160 {rew_ord'="tless_true",rls'=tval_rls, |
|
161 srls=append_rls "testlet_srls" e_rls |
|
162 [Calc ("Test.contains'_root",eval_contains_root"")], |
|
163 prls=e_rls,calc=[],asm_rls=[],asm_thm=[("square_equation_left","")]}, |
|
164 "Script Testeq2 (e_::bool) = \ |
|
165 \(let e_ =\ |
|
166 \ ((While (contains_root e_) Do \ |
|
167 \ (Rewrite square_equation_left True))\ |
|
168 \ e_)\ |
|
169 \in [e_::bool])" |
|
170 ) |
|
171 ]); |
|
172 val Script sc = (#scr o get_met) ("Test.thy","testlet"); |
|
173 writeln(term2str sc); |
|
174 val fmz = ["boolTestGiven (sqrt a = 0)", |
|
175 "boolTestFind v_i_"]; |
|
176 val (dI',pI',mI') = ("Test.thy",["met-testeq","tests"], |
|
177 ("Test.thy","testlet")); |
|
178 val p = e_pos'; val c = []; |
|
179 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
180 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree; |
|
181 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
182 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
183 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
184 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
185 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
186 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testlet"))*) |
|
187 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
188 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
189 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
190 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso |
|
191 nxt=("End_Proof'",End_Proof') then () |
|
192 else raise error "different behaviour in test 11.5.02 Testeq: let e_ =... in [e_]"; |
|
193 |
|
194 |
|
195 |
|
196 |
|
197 " _________________ me + nxt_step from script _________________ "; |
|
198 " _________________ me + nxt_step from script _________________ "; |
|
199 " _________________ me + nxt_step from script _________________ "; |
|
200 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
201 "solveFor x","errorBound (eps=0)", |
|
202 "solutions L"]; |
|
203 val (dI',pI',mI') = |
|
204 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
205 ("Test.thy","sqrt-equ-test")); |
|
206 val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test"); |
|
207 writeln(term2str sc); |
|
208 |
|
209 val p = e_pos'; val c = []; |
|
210 "--- s1 ---"; |
|
211 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
212 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
213 "--- s2 ---"; |
|
214 (* val nxt = |
|
215 ("Add_Given", |
|
216 Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*) |
|
217 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
218 "--- s3 ---"; |
|
219 (* val nxt = ("Add_Given",Add_Given "solveFor x");*) |
|
220 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
221 "--- s4 ---"; |
|
222 (* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*) |
|
223 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
224 "--- s5 ---"; |
|
225 (* val nxt = ("Add_Find",Add_Find "solutions L");*) |
|
226 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
227 "--- s6 ---"; |
|
228 (* val nxt = ("Specify_Domain",Specify_Domain "Test.thy");*) |
|
229 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
230 "--- s7 ---"; |
|
231 (* val nxt = |
|
232 ("Specify_Problem", |
|
233 Specify_Problem ["sqroot-test","univariate","equation","test"]);*) |
|
234 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
235 "--- s8 ---"; |
|
236 (* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*) |
|
237 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
238 "--- s9 ---"; |
|
239 (* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*) |
|
240 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
241 "--- 1 ---"; |
|
242 (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*) |
|
243 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
244 "--- 2 ---"; |
|
245 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) |
|
246 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
247 "--- 3 ---"; |
|
248 (* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*) |
|
249 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
250 "--- 4 ---"; |
|
251 (* val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");*) |
|
252 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
253 "--- 5 ---"; |
|
254 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) |
|
255 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
256 "--- 6 ---"; |
|
257 (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*) |
|
258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
259 "--- 7 ---"; |
|
260 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) |
|
261 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
262 "--- 8<> ---"; |
|
263 (* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*) |
|
264 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
265 "--- 9<> ---"; |
|
266 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) |
|
267 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
268 "--- 10<> ---"; |
|
269 (* val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");*) |
|
270 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
271 "--- 11<> ---"; |
|
272 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) |
|
273 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
274 "--- 12<> ---."; |
|
275 (* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));*) |
|
276 get_form nxt p pt; |
|
277 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
278 "--- 13<> ---"; |
|
279 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) |
|
280 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
281 "--- 14<> ---"; |
|
282 (* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*) |
|
283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
284 if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) |
|
285 then raise error "scriptnew.sml 1: me + msteps from script: new behaviour" |
|
286 else (); |
|
287 "--- 15<> ---"; |
|
288 (* val nxt = ("End_Proof'",End_Proof');*) |
|
289 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
290 |
|
291 writeln (pr_ptree pr_short pt); |
|
292 writeln("result: "^(get_obj g_result pt [])^ |
|
293 "\n============================================================="); |
|
294 (*get_obj g_asm pt []; |
|
295 val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*) |
|
296 |
|
297 |
|
298 |
|
299 |
|
300 |
|
301 " _________________ me + sqrt-equ-test: 1.norm_equation _________________ "; |
|
302 " _________________ me + sqrt-equ-test: 1.norm_equation _________________ "; |
|
303 " _________________ me + sqrt-equ-test: 1.norm_equation _________________ "; |
|
304 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
305 "solveFor x","errorBound (eps=0)", |
|
306 "solutions L"]; |
|
307 val (dI',pI',mI') = |
|
308 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
309 ("Test.thy","sqrt-equ-test")); |
|
310 val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test"); |
|
311 (writeln o term2str) sc; |
|
312 val p = e_pos'; val c = []; |
|
313 "--- s1 ---"; |
|
314 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
315 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
316 "--- s2 ---"; |
|
317 (* val nxt = ("Add_Given", |
|
318 Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*) |
|
319 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
320 "--- s3 ---"; |
|
321 (* val nxt = ("Add_Given",Add_Given "solveFor x");*) |
|
322 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
323 "--- s4 ---"; |
|
324 (* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*) |
|
325 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
326 "--- s5 ---"; |
|
327 (* val nxt = ("Add_Find",Add_Find "solutions L");*) |
|
328 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
329 "--- s6 ---"; |
|
330 (* val nxt = ("Specify_Domain",Specify_Domain "Test.thy");*) |
|
331 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
332 "--- s7 ---"; |
|
333 (* val nxt = ("Specify_Problem", |
|
334 Specify_Problem ["sqroot-test","univariate","equation","test"]);*) |
|
335 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
336 "--- s8 ---"; |
|
337 (* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*) |
|
338 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
339 "--- s9 ---"; |
|
340 (* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*) |
|
341 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
342 "--- !!! x1 --- 1.norm_equation"; |
|
343 (*###*)val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation"); |
|
344 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
345 "--- !!! x2 --- 1.norm_equation"; |
|
346 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) |
|
347 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
348 (*(me nxt p [1] pt) handle e => print_exn_G e;*) |
|
349 "--- !!! x3 --- 1.norm_equation"; |
|
350 (*val nxt = ("Empty_Mstep",Empty_Mstep) ### helpless*) |
|
351 (*###*)val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc"); |
|
352 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
353 "--- !!! x4 --- 1.norm_equation"; |
|
354 (*val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root")*) |
|
355 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
356 "--- !!! x5 --- 1.norm_equation"; |
|
357 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) |
|
358 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
359 if f= Form'(FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)")) |
|
360 then() else raise error "new behaviour in test-example 1.norm sqrt-equ-test"; |
|
361 |
|
362 |
|
363 (* use"../tests/scriptnew.sml"; |
|
364 *) |
|
365 |
|
366 " _________________ equation with x =(-12)/5, but L ={} ------- "; |
|
367 |
|
368 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))", |
|
369 "solveFor x","errorBound (eps=0)", |
|
370 "solutions L"]; |
|
371 val (dI',pI',mI') = |
|
372 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
373 ("Test.thy","square_equation")); |
|
374 val p = e_pos'; val c = []; |
|
375 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
376 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
377 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
378 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
379 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
380 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
381 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
382 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
383 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
384 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
385 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
386 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
387 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
388 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
389 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
390 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
391 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
392 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
393 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
394 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
395 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
396 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
398 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
399 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
400 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
401 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
402 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
403 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
404 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
405 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
406 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
407 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
408 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
409 trace_rewrite:=true; |
|
410 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
411 |
|
412 trace_rewrite:=false; |
|
413 |
|
414 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
415 val Form' (FormKF (_,_,_,_,ff)) = f; |
|
416 if ff="[]" then () |
|
417 else raise error "diff.behav. in scriptnew.sml; root-eq: L = []"; |
|
418 |
|
419 |
|
420 val tt = (term_of o the o (parse thy)) "?xxx"; |
|
421 rewrite_set_ thy true tval_rls ; |