|
1 (* use"test-FE-KE.sml"; |
|
2 W.N.16.4.00 |
|
3 *) |
|
4 |
|
5 (*contents*) |
|
6 " _________________ stdin: tutor active_________________ "; |
|
7 " _________________ stdin: student active_________________ "; |
|
8 " _________________ stdin: root_equ: 1.norm_equation ________________ "; |
|
9 " _________________ stdin: root_equ: spec_hide ________________ "; |
|
10 " ------------- test-FE-KE.sml: test100 ------------- "; |
|
11 " _________________ stdin: root_equ: Auto ________________ "; |
|
12 (*contents*) |
|
13 |
|
14 |
|
15 |
|
16 |
|
17 (*#########################################################*) |
|
18 " _________________ stdin: tutor active_________________ "; |
|
19 " _________________ stdin: tutor active_________________ "; |
|
20 " _________________ stdin: tutor active_________________ "; |
|
21 " _________________ stdin: tutor active_________________ "; |
|
22 " _________________ stdin: tutor active_________________ "; |
|
23 " _________________ stdin: tutor active_________________ "; |
|
24 proofs:= []; dials:=([],[],[]); |
|
25 StdinSML 0 0 0 0 New_User; |
|
26 set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*) |
|
27 StdinSML 1 0 0 0 New_Proof; |
|
28 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
29 "solveFor x","errorBound (eps=0)", |
|
30 "solutions L"]; |
|
31 val (dI',pI',mI') = |
|
32 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
33 ("Test.thy","sqrt-equ-test")); |
|
34 "--- s1 ---"; |
|
35 val (_,1,1,1,[],[_,_,PpcKF (_,_,_,_,ppc),req],_) = |
|
36 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
37 "--- s2 ---"; |
|
38 StdinSML 1 1 ~1 ~1 (Command Accept); |
|
39 (*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*) |
|
40 "--- s3 ---"; |
|
41 StdinSML 1 1 ~2 ~2 (Command Accept); |
|
42 (*RuleFK (Add_Given "solveFor x")*) |
|
43 "--- s4 ---"; |
|
44 StdinSML 1 1 ~3 ~3 (Command Accept); |
|
45 (*RuleFK (Add_Given "errorBound (eps = #0)")*) |
|
46 "--- s5 ---"; |
|
47 StdinSML 1 1 ~4 ~4 (Command Accept); |
|
48 (*RuleFK (Add_Find "solutions L")*) |
|
49 "--- s6 ---"; |
|
50 StdinSML 1 1 ~5 ~5 (Command Accept); |
|
51 (*RuleFK (Specify_Domain "Test.thy")*) |
|
52 "--- s7 ---"; |
|
53 StdinSML 1 1 ~6 ~6 (Command Accept); |
|
54 (*RuleFK (Specify_Problem ["sqroot-test","univariate","equation","test"])*) |
|
55 "--- s8 ---"; |
|
56 StdinSML 1 1 ~7 ~7 (Command Accept); |
|
57 (*RuleFK (Specify_Method ("Test.thy","sqrt-equ-test"))*) |
|
58 "--- s9 ---"; |
|
59 val (_,1,1,~8,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
60 StdinSML 1 1 ~8 ~8 (Command Accept); |
|
61 if ct'="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)" andalso |
|
62 r = Apply_Method ("Test.thy","sqrt-equ-test") |
|
63 then () else raise error "new behaviour in test-example"; |
|
64 (*RuleFK (Apply_Method ("Test.thy","sqrt-equ-test"))*) |
|
65 |
|
66 "--- 1 ---"; |
|
67 val (_,1,1,~9,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
68 StdinSML 1 1 ~9 ~9 (Command Accept); |
|
69 (*RuleFK (Rewrite ("square_equation_left",""))*) |
|
70 "--- 2 ---"; |
|
71 val (_,1,1,~10,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
72 StdinSML 1 1 ~10 ~10 (Command Accept); |
|
73 (*RuleFK (Rewrite_Set "Test_simplify")*) |
|
74 "--- 3 ---"; |
|
75 val (_,1,1,~11,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
76 StdinSML 1 1 ~11 ~11 (Command Accept); |
|
77 (*RuleFK (Rewrite_Set "rearrange_assoc")*) |
|
78 "--- 4 ---"; |
|
79 val (_,1,1,~12,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
80 StdinSML 1 1 ~12 ~12 (Command Accept); |
|
81 (*RuleFK (Rewrite_Set "isolate_root")*) |
|
82 "--- 5 ---"; |
|
83 val (_,1,1,~13,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
84 StdinSML 1 1 ~13 ~13 (Command Accept); |
|
85 (*RuleFK (Rewrite_Set "Test_simplify")*) |
|
86 "--- 6 ---"; |
|
87 val (_,1,1,~14,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
88 StdinSML 1 1 ~14 ~14 (Command Accept); |
|
89 (*RuleFK (Rewrite ("square_equation_left",""))*) |
|
90 "--- 7 ---"; |
|
91 val (_,1,1,~15,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
92 StdinSML 1 1 ~15 ~15 (Command Accept); |
|
93 (*RuleFK (Rewrite_Set "Test_simplify")*) |
|
94 "--- 8 ---"; |
|
95 val (_,1,1,~16,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
96 StdinSML 1 1 ~16 ~16 (Command Accept); |
|
97 (*val r = Rewrite_Set "rearrange_assoc"*) |
|
98 "--- 9 ---"; |
|
99 val (_,1,1,~17,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
100 StdinSML 1 1 ~17 ~17 (Command Accept); |
|
101 (*RuleFK (Rewrite_Set "Test_simplify")*) |
|
102 "--- 10 ---"; |
|
103 val (_,1,1,~18,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
104 StdinSML 1 1 ~18 ~18 (Command Accept); |
|
105 (*val r = Rewrite_Set "norm_equation"*) |
|
106 "--- 11 ---"; |
|
107 val (_,1,1,~19,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
108 StdinSML 1 1 ~19 ~19 (Command Accept); |
|
109 (*RuleFK (Rewrite_Set "Test_simplify")*) |
|
110 "--- 13 ---"; |
|
111 val (_,1,1,~20,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
112 StdinSML 1 1 ~20 ~20 (Command Accept); |
|
113 (*RuleFK (Rewrite_Set_Inst ([(#,#)],"isolate_bdv"))*) |
|
114 "--- 14 ---"; |
|
115 val (_,1,1,~21,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
116 StdinSML 1 1 ~21 ~21 (Command Accept); |
|
117 (*RuleFK (Rewrite_Set "Test_simplify")*) |
|
118 "--- 15 ---"; |
|
119 val (_,1,1,~22,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = |
|
120 StdinSML 1 1 ~22 ~22 (Command Accept); |
|
121 "--- 16 ---"; |
|
122 val (_,1,1,~23,[],[req,End_Proof],_) = |
|
123 StdinSML 1 1 ~23 ~23 (Command Accept); |
|
124 |
|
125 (* |
|
126 "=====================";======================= |
|
127 use"test-FE-KE.sml"; |
|
128 *) |
|
129 |
|
130 |
|
131 (*#########################################################*) |
|
132 " _________________ stdin: student active_________________ "; |
|
133 " _________________ stdin: student active_________________ "; |
|
134 " _________________ stdin: student active_________________ "; |
|
135 " _________________ stdin: student active_________________ "; |
|
136 " _________________ stdin: student active_________________ "; |
|
137 " _________________ stdin: student active_________________ "; |
|
138 proofs:= []; dials:=([],[],[]); |
|
139 StdinSML 0 0 0 0 New_User; |
|
140 set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*) |
|
141 (*SelRule WORKS BY CAHCNE, and wrong, IN SPECIFY*) |
|
142 StdinSML 1 0 0 0 New_Proof; |
|
143 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
144 "solveFor x","errorBound (eps=0)", |
|
145 "solutions L"]; |
|
146 val (dI',pI',mI') = |
|
147 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
148 ("Test.thy","sqrt-equ-test")); |
|
149 "--- s1 ---"; |
|
150 val (_,1,1,1,[],[_,_,PpcKF (_,_,_,_,f), Select _, req],_) = |
|
151 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
152 "--- s2 ---"; |
|
153 (*val (_,1,1,~1,[],[PpcKF (_,_,_,_,ppc),RuleKF (_,r),req],_) = *) |
|
154 StdinSML 1 1 ~1 ~1 |
|
155 (RuleFK (Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))")); |
|
156 "--- s3 ---"; |
|
157 StdinSML 1 1 ~2 ~2 (RuleFK (Add_Given "solveFor x")); |
|
158 "--- s4 ---"; |
|
159 StdinSML 1 1 ~3 ~3 (RuleFK (Add_Given "errorBound (eps = 0)")); |
|
160 "--- s5 ---"; |
|
161 StdinSML 1 1 ~4 ~4 (RuleFK (Add_Find "solutions L")); |
|
162 "--- s6 ---"; |
|
163 StdinSML 1 1 ~5 ~5 (RuleFK (Specify_Domain "Test.thy")); |
|
164 "--- s7 ---"; |
|
165 StdinSML 1 1 ~6 ~6 (RuleFK |
|
166 (Specify_Problem ["sqroot-test","univariate","equation","test"])); |
|
167 "--- s8 ---"; |
|
168 StdinSML 1 1 ~7 ~7 (RuleFK (Specify_Method ("Test.thy","sqrt-equ-test"))); |
|
169 "--- s9 ---"; |
|
170 StdinSML 1 1 ~8 ~8 (RuleFK (Apply_Method ("Test.thy","sqrt-equ-test"))); |
|
171 "--- 1 ---"; |
|
172 StdinSML 1 1 ~9 ~9 (RuleFK (Rewrite ("square_equation_left",""))); |
|
173 "--- 2 ---"; |
|
174 StdinSML 1 1 ~10 ~10 (RuleFK (Rewrite_Set "Test_simplify")); |
|
175 "--- 3 ---"; |
|
176 StdinSML 1 1 ~11 ~11 (RuleFK (Rewrite_Set "rearrange_assoc")); |
|
177 "--- 4 ---"; |
|
178 StdinSML 1 1 ~12 ~12 (RuleFK (Rewrite_Set "isolate_root")); |
|
179 "--- 5 ---"; |
|
180 StdinSML 1 1 ~13 ~13 (RuleFK (Rewrite_Set "Test_simplify")); |
|
181 "--- 6 ---"; |
|
182 StdinSML 1 1 ~14 ~14 (RuleFK |
|
183 (Rewrite ("square_equation_left",""))); |
|
184 "--- 7 ---"; |
|
185 StdinSML 1 1 ~15 ~15 (RuleFK (Rewrite_Set "Test_simplify")); |
|
186 "--- 8<> ---"; |
|
187 StdinSML 1 1 ~16 ~16 (RuleFK (Rewrite_Set "rearrange_assoc")); |
|
188 "--- 9<> ---"; |
|
189 StdinSML 1 1 ~17 ~17 (RuleFK (Rewrite_Set "Test_simplify")); |
|
190 "--- 10<> ---"; |
|
191 StdinSML 1 1 ~18 ~18 (RuleFK (Rewrite_Set "norm_equation")); |
|
192 "--- 11<> ---"; |
|
193 StdinSML 1 1 ~19 ~19 (RuleFK (Rewrite_Set "Test_simplify")); |
|
194 "--- 12<> ---"; |
|
195 StdinSML 1 1 ~20 ~20 (RuleFK |
|
196 (Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"))); |
|
197 "--- 13<> ---"; |
|
198 StdinSML 1 1 ~21 ~21 (RuleFK (Rewrite_Set "Test_simplify")); |
|
199 "--- 14<> ---"; |
|
200 val (begin,uI,pI,acI,cI,dats,eend) = |
|
201 StdinSML 1 1 ~22 ~22 (RuleFK |
|
202 (Check_Postcond ["sqroot-test","univariate","equation","test"])); |
|
203 |
|
204 |
|
205 (* |
|
206 "=====================";======================= |
|
207 use"test-FE-KE.sml"; |
|
208 *) |
|
209 |
|
210 |
|
211 |
|
212 |
|
213 " _________________ stdin: root_equ: 1.norm_equation ________________ "; |
|
214 " _________________ stdin: root_equ: 1.norm_equation ________________ "; |
|
215 " _________________ stdin: root_equ: 1.norm_equation ________________ "; |
|
216 " _________________ stdin: root_equ: 1.norm_equation ________________ "; |
|
217 " _________________ stdin: root_equ: 1.norm_equation ________________ "; |
|
218 " _________________ stdin: root_equ: 1.norm_equation ________________ "; |
|
219 proofs:= []; dials:=([],[],[]); |
|
220 StdinSML 0 0 0 0 New_User; |
|
221 set_dstate 1 test_hide 0 2; |
|
222 StdinSML 1 0 0 0 New_Proof; |
|
223 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
224 "solveFor x","errorBound (eps=0)", |
|
225 "solutions L"]; |
|
226 val (dI',pI',mI') = |
|
227 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
228 ("Test.thy","sqrt-equ-test")); |
|
229 "--- s1 ---"; |
|
230 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
231 "--- s2 ---"; |
|
232 StdinSML 1 1 ~1 ~1 (Command Accept); |
|
233 (*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*) |
|
234 "--- s3 ---"; |
|
235 StdinSML 1 1 ~2 ~2 (Command Accept); |
|
236 (*RuleFK (Add_Given "solveFor x")*) |
|
237 "--- s4 ---"; |
|
238 StdinSML 1 1 ~3 ~3 (Command Accept); |
|
239 (*RuleFK (Add_Given "errorBound (eps = #0)")*) |
|
240 "--- s5 ---"; |
|
241 StdinSML 1 1 ~4 ~4 (Command Accept); |
|
242 (*RuleFK (Add_Find "solutions L")*) |
|
243 "--- s6 ---"; |
|
244 StdinSML 1 1 ~5 ~5 (Command Accept); |
|
245 (*RuleFK (Specify_Domain "Test.thy")*) |
|
246 "--- s7 ---"; |
|
247 StdinSML 1 1 ~6 ~6 (Command Accept); |
|
248 (*RuleFK (Specify_Problem ["sqroot-test","univariate","equation","test"])*) |
|
249 "--- s8 ---"; |
|
250 StdinSML 1 1 ~7 ~7 (Command Accept); |
|
251 (*RuleFK (Specify_Method ("Test.thy","sqrt-equ-test"))*) |
|
252 "--- s9 ---"; |
|
253 val (_,1,1,~8,[],[RuleKF (_,r),FormKF (_,_,_,_,f),req],_) = |
|
254 StdinSML 1 1 ~8 ~8 (Command Accept); |
|
255 (*RuleFK (Apply_Method ("Test.thy","sqrt-equ-test"))*) |
|
256 "--- !!! x1 --- strange choice"; |
|
257 StdinSML 1 1 ~9 2 (RuleFK (Rewrite_Set "norm_equation")); |
|
258 "--- !!! x2 --- ME knows nxt_step"; |
|
259 StdinSML 1 1 ~10 3 (RuleFK (Rewrite_Set "Test_simplify")); |
|
260 "--- !!! x3 --- helpless !!!"; |
|
261 StdinSML 1 1 ~11 4 (RuleFK (Rewrite_Set "rearrange_assoc")); |
|
262 "--- !!! x4 ---"; |
|
263 StdinSML 1 1 ~12 5 (RuleFK (Rewrite_Set "isolate_root")); |
|
264 "--- !!! x5 --- back at original equation !!!"; |
|
265 val (_,_,_,_,_,[FormKF (_,_,_,_,res),requ],_) = |
|
266 StdinSML 1 1 ~13 5 (RuleFK (Rewrite_Set "Test_simplify")); |
|
267 if res="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)" |
|
268 then () else raise error "new behaviour in 1.norm_equ"; |
|
269 |
|
270 (* |
|
271 "=====================================";=====@@@@@s===== |
|
272 use"test-FE-KE.sml"; |
|
273 W.N.16.4.00 |
|
274 *) |
|
275 |
|
276 " _________________ stdin: root_equ: spec_hide ________________ "; |
|
277 " _________________ stdin: root_equ: spec_hide ________________ "; |
|
278 " _________________ stdin: root_equ: spec_hide ________________ "; |
|
279 " _________________ stdin: root_equ: spec_hide ________________ "; |
|
280 " _________________ stdin: root_equ: spec_hide ________________ "; |
|
281 " _________________ stdin: root_equ: spec_hide ________________ "; |
|
282 " _________________ stdin: root_equ: spec_hide ________________ "; |
|
283 proofs:= []; dials:=([],[],[]); |
|
284 StdinSML 0 0 0 0 New_User; |
|
285 set_dstate 1 spec_hide 4 1; |
|
286 StdinSML 1 0 0 0 New_Proof; |
|
287 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
288 "solveFor x","errorBound (eps=0)", |
|
289 "solutions L"]; |
|
290 val (dI',pI',mI') = |
|
291 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
292 ("Test.thy","sqrt-equ-test")); |
|
293 val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test"); |
|
294 writeln(term2str sc); |
|
295 "--- s1 ---"; |
|
296 val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),Select _,req],_) = |
|
297 |
|
298 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
299 "--- !!! x1 --- strange choice"; (*TODO 31.10.00: hier nochmals spec ?!?!?*) |
|
300 StdinSML 1 1 ~1 ~1 (RuleFK (Rewrite_Set "norm_equation")); |
|
301 "--- !!! x2 --- ME knows nxt_step"; |
|
302 StdinSML 1 1 ~2 ~2 (RuleFK (Rewrite_Set "Test_simplify")); |
|
303 "--- !!! x3 --- helpless !!!"; |
|
304 val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = |
|
305 StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Set "rearrange_assoc")); |
|
306 "--- !!! x4 ---"; |
|
307 val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = |
|
308 StdinSML 1 1 ~4 ~4 (RuleFK (Rewrite_Set "isolate_root")); |
|
309 "--- !!! x5 --- back at original equation !!!"; |
|
310 val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = |
|
311 |
|
312 StdinSML 1 1 ~5 ~5 (RuleFK (Rewrite_Set "Test_simplify")); |
|
313 if res="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)" |
|
314 then () else raise error "new behaviour in test-example"; |
|
315 |
|
316 "--- !!! x6 --- not applicable"; |
|
317 val (_,_,_,_,_,[Error_ err,Select _,requ],_) = |
|
318 StdinSML 1 1 ~6 ~6 (RuleFK (Rewrite_Set "Test_simplify")); |
|
319 |
|
320 val (_,_,_,_,_,[RuleKF r,FormKF (_,_,_,_,f),requ],_) = |
|
321 StdinSML 1 1 ~6 ~6 (Command YourTurn); |
|
322 |
|
323 StdinSML 1 1 ~7 ~7 (Command ActiveMinus); |
|
324 StdinSML 1 1 ~7 ~7 (Command ActiveMinus); |
|
325 StdinSML 1 1 ~7 ~7 (Command ActiveMinus); |
|
326 StdinSML 1 1 ~7 ~7 (Command ActiveMinus);(*acti=0*) |
|
327 StdinSML 1 1 ~7 ~7 (Command SpeedPlus);(*speed=2:PutRule,TskipS..PutRuleRes,Tt.*) |
|
328 StdinSML 1 1 ~7 ~7 (Command Accept); |
|
329 StdinSML 1 1 ~8 ~8 (Command Accept); |
|
330 StdinSML 1 1 ~9 ~9 (Command Accept); |
|
331 StdinSML 1 1 ~10 ~10 (Command Accept); |
|
332 StdinSML 1 1 ~11 ~11 (Command Accept); |
|
333 StdinSML 1 1 ~12 ~12 (Command Accept); |
|
334 StdinSML 1 1 ~13 ~13 (Command Accept); |
|
335 StdinSML 1 1 ~14 ~14 (Command Accept); |
|
336 |
|
337 (*17.9.02: nach Umbau KB wird Equ immer gr"osser ?!----- |
|
338 StdinSML 1 1 ~15 ~15 (Command Accept); |
|
339 StdinSML 1 1 ~16 ~16 (Command Accept); |
|
340 StdinSML 1 1 ~17 ~17 (Command Accept); |
|
341 StdinSML 1 1 ~18 ~18 (Command Accept); |
|
342 val (_,1,1,_,_,[FormKF (~20,_,0,_,f),req],_) = |
|
343 StdinSML 1 1 ~19 ~19 (Command Accept); |
|
344 if f="[x = 4]" then () else raise error "new behaviour in test-example"; |
|
345 |
|
346 val (_,1,1,~20,[],[Request "start another example",End_Proof],_) = |
|
347 StdinSML 1 1 ~20 ~20 (Command Accept); |
|
348 --------------------------------------------------------------------*) |
|
349 |
|
350 (* |
|
351 "=====================================";=====@@@@@===== |
|
352 use"test-FE-KE.sml"; |
|
353 *) |
|
354 |
|
355 |
|
356 " ------------- test-FE-KE.sml: test100 ------------- "; |
|
357 " ------------- test-FE-KE.sml: test100 ------------- "; |
|
358 " ------------- test-FE-KE.sml: test100 ------------- "; |
|
359 " ------------- test-FE-KE.sml: test100 ------------- "; |
|
360 " ------------- test-FE-KE.sml: test100 ------------- "; |
|
361 " ------------- test-FE-KE.sml: test100 ------------- "; |
|
362 StdinSML 0 0 0 0 New_User; |
|
363 StdinSML 1 0 0 0 New_Proof; |
|
364 val fmz = ["realTestGiven (0+0)*(1*(1*a))", |
|
365 "realTestFind a"]; |
|
366 val (dI',pI',mI') = |
|
367 ("Script.thy",["Script.thy","pbl-testterm"], |
|
368 ("Script.thy","met-testterm")); |
|
369 "--- s1 ---"; |
|
370 (* |
|
371 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
372 *** Type unification failed: Clash of types "Descript.una" and "RealDef.real". |
|
373 *) |
|
374 "--- s2 ---"; |
|
375 (*too many problems with setup of this example*) |
|
376 |
|
377 |
|
378 " _________________ stdin: root_equ: Auto ________________ "; |
|
379 " _________________ stdin: root_equ: Auto ________________ "; |
|
380 " _________________ stdin: root_equ: Auto ________________ "; |
|
381 " _________________ stdin: root_equ: Auto ________________ "; |
|
382 " _________________ stdin: root_equ: Auto ________________ "; |
|
383 proofs:= []; dials:=([],[],[]); |
|
384 StdinSML 0 0 0 0 New_User; |
|
385 set_dstate 1 spec_hide 4 1; |
|
386 StdinSML 1 0 0 0 New_Proof; |
|
387 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
388 "solveFor x","errorBound (eps=0)", |
|
389 "solutions L"]; |
|
390 val (dI',pI',mI') = |
|
391 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
392 ("Test.thy","sqrt-equ-test")); |
|
393 "--- s1 ---"; |
|
394 val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),Select _,req],_) = |
|
395 StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); |
|
396 |
|
397 val (_,1,1,~1,[], |
|
398 [RuleKF _,_,_,_,_,_,_,_,_,_,_,_,_,_,_,req,End_Proof],_) = |
|
399 StdinSML 1 1 ~1 ~1 (Command Auto); |
|
400 |
|
401 |
|
402 |
|
403 "######################### test-FE_KE.sml complete #####################"; |