245 val d = e_rls; |
245 val d = e_rls; |
246 |
246 |
247 " --- test100: nxt_tac order------------------------------------ "; |
247 " --- test100: nxt_tac order------------------------------------ "; |
248 " --- test100: nxt_tac order------------------------------------ "; |
248 " --- test100: nxt_tac order------------------------------------ "; |
249 |
249 |
250 val scr as (Script sc) = Script (((inst_abs Test.thy) |
250 val scr as (Prog sc) = Prog (((inst_abs Test.thy) |
251 o term_of o the o (parse thy)) |
251 o term_of o the o (parse thy)) |
252 "Script Testeq (e_e::bool) = \ |
252 "Script Testeq (e_e::bool) = \ |
253 \(While (contains_root e_e) Do \ |
253 \(While (contains_root e_e) Do \ |
254 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ |
254 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ |
255 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ |
255 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ |
279 (*12.10.03:*** Unknown theorem(s) "rroot_square_inv" |
279 (*12.10.03:*** Unknown theorem(s) "rroot_square_inv" |
280 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); |
280 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); |
281 *) |
281 *) |
282 |
282 |
283 |
283 |
284 val scr as (Script sc) = |
284 val scr as (Prog sc) = |
285 Script (((inst_abs Test.thy) o term_of o the o (parse thy)) |
285 Prog (((inst_abs Test.thy) o term_of o the o (parse thy)) |
286 "Script Testterm (g_::real) = (Calculate cancel g_)"); |
286 "Script Testterm (g_::real) = (Calculate cancel g_)"); |
287 (* |
287 (* |
288 val scr as (Script sc) = |
288 val scr as (Prog sc) = |
289 Script (((inst_abs Test.thy) o term_of o the o (parse thy)) |
289 Prog (((inst_abs Test.thy) o term_of o the o (parse thy)) |
290 "Script Testterm (g_::real) = (Calculate power g_)"); |
290 "Script Testterm (g_::real) = (Calculate power g_)"); |
291 val scr as (Script sc) = |
291 val scr as (Prog sc) = |
292 Script (((inst_abs Test.thy) o term_of o the o (parse thy)) |
292 Prog (((inst_abs Test.thy) o term_of o the o (parse thy)) |
293 "Script Testterm (g_::real) = (Calculate pow g_)"); |
293 "Script Testterm (g_::real) = (Calculate pow g_)"); |
294 ..............................................................*) |
294 ..............................................................*) |
295 writeln |
295 writeln |
296 "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\ |
296 "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\ |
297 \ (Repeat (Calculate cancel g_)) Or \n\ |
297 \ (Repeat (Calculate cancel g_)) Or \n\ |