1.1 --- a/src/Tools/isac/Test_Isac.thy Tue Oct 05 09:01:30 2010 +0200
1.2 +++ b/src/Tools/isac/Test_Isac.thy Tue Oct 05 09:17:48 2010 +0200
1.3 @@ -1,6 +1,7 @@
1.4 (* Title Run_Tests on isac
1.5 $ cd /usr/local/isabisac/test/Tools/isac
1.6 $ /usr/local/isabisac/bin/isabelle emacs -l Isac Test_Isac.thy &
1.7 +$ /usr/local/isabisac/bin/isabelle emacs Test_Isac.thy &
1.8
1.9 RESTART emacs after having created a new Isac heap.
1.10 was sml/RTEST-root.sml in isac-2002
2.1 --- a/test/Tools/isac/Interpret/me.sml Tue Oct 05 09:01:30 2010 +0200
2.2 +++ b/test/Tools/isac/Interpret/me.sml Tue Oct 05 09:17:48 2010 +0200
2.3 @@ -427,7 +427,7 @@
2.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.7 - val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
2.8 + val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
2.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.11 (*nxt = Specify_Theory "DiffApp.thy"*)
3.1 --- a/test/Tools/isac/Interpret/ptyps.sml Tue Oct 05 09:01:30 2010 +0200
3.2 +++ b/test/Tools/isac/Interpret/ptyps.sml Tue Oct 05 09:17:48 2010 +0200
3.3 @@ -365,7 +365,7 @@
3.4 With=[]}))) : mout
3.5 val nxt = ("Add_Find",Add_Find "solutions L") ????!!!!????*)
3.6
3.7 -val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
3.8 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
3.9 val (p,_,f,nxt,_,pt) = me nxt p c pt(*NEW2*);
3.10 (*val nxt = ("Empty_Tac",Empty_Tac)
3.11 ... Refine_Problem ["linear"..] fails internally 040312: works!?!*)
4.1 --- a/test/Tools/isac/Interpret/solve.sml Tue Oct 05 09:01:30 2010 +0200
4.2 +++ b/test/Tools/isac/Interpret/solve.sml Tue Oct 05 09:17:48 2010 +0200
4.3 @@ -203,7 +203,7 @@
4.4 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*)
4.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
4.6 val nxt = ("Detail",Detail);"----------------------";
4.7 - val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
4.8 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
4.9 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.10 (*15.10.02*)
4.11 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.12 @@ -214,7 +214,7 @@
4.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.16 - val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
4.17 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
4.18 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.19 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)"))
4.20 andalso nxt = ("End_Proof'",End_Proof') then ()
4.21 @@ -336,13 +336,13 @@
4.22 (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*)
4.23 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*)
4.24 val nxt = ("Detail",Detail);"----------------------";
4.25 - val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
4.26 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
4.27 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.28 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.29 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.30 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.31 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.32 - val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e;
4.33 + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => OldGoals.print_exn e;
4.34 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
4.35 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)"))
4.36 andalso nxt = ("End_Proof'",End_Proof') then ()
5.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Tue Oct 05 09:01:30 2010 +0200
5.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Tue Oct 05 09:17:48 2010 +0200
5.3 @@ -274,7 +274,7 @@
5.4 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.7 -val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
5.8 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
5.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.12 @@ -373,7 +373,7 @@
5.13
5.14 (*----postponed.15.5.03 run scripts for maximum-example: univariate equation
5.15
5.16 -val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
5.17 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
5.18
5.19 val oris = fst3 (get_obj g_origin pt (fst p));writeln(oris2str oris);
5.20
6.1 --- a/test/Tools/isac/Knowledge/rational-old.sml Tue Oct 05 09:01:30 2010 +0200
6.2 +++ b/test/Tools/isac/Knowledge/rational-old.sml Tue Oct 05 09:17:48 2010 +0200
6.3 @@ -290,7 +290,7 @@
6.4 print("c)\n");
6.5 val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )";
6.6 val e186c = (the (rewrite_set thy' "rational_erls" false rls' e186c'))
6.7 - handle e => print_exn e;
6.8 + handle e => OldGoals.print_exn e;
6.9 val t = (term_of o the o (parse thy)) e186c';
6.10 atomt t;
6.11
6.12 @@ -735,7 +735,7 @@
6.13 val t = (term_of o the o (parse thy))
6.14 "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
6.15 val thm = (mk_thm thy "(-6) * x = 2 * ((-3) * x)")
6.16 - handle e => print_exn e;
6.17 + handle e => OldGoals.print_exn e;
6.18 val SOME (t',_) = rewrite_ thy e_rew_ord e_rls false thm t;
6.19 term2str t';
6.20 ----------------------------------------------------------------------*)
7.1 --- a/test/Tools/isac/Knowledge/rational.sml Tue Oct 05 09:01:30 2010 +0200
7.2 +++ b/test/Tools/isac/Knowledge/rational.sml Tue Oct 05 09:17:48 2010 +0200
7.3 @@ -489,7 +489,7 @@
7.4 writeln("c)");
7.5 val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )";
7.6 val e186c = (the (rewrite_set thy' false "cancel" e186c'))
7.7 - handle e => print_exn e;
7.8 + handle e => OldGoals.OldGoals.print_exn e;
7.9 val t = (term_of o the o (parse thy)) e186c';
7.10 atomt t;
7.11
8.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Tue Oct 05 09:01:30 2010 +0200
8.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Tue Oct 05 09:17:48 2010 +0200
8.3 @@ -195,7 +195,7 @@
8.4 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testlet"))*)
8.5 val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.6 val (p,_,f,nxt,_,pt) = me nxt p c pt;
8.7 -val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
8.8 +val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => OldGoals.print_exn e;
8.9 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso
8.10 nxt=("End_Proof'",End_Proof') then ()
8.11 else error "different behaviour in test 11.5.02 Testeq: let e_e =... in [e_]";