1.1 --- a/test/Tools/isac/Knowledge/diff.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diff.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -108,7 +108,7 @@
1.4 (*got: false instead true; ~~~~~~~~~~~ replaced by 'is_atom'*)
1.5 val SOME (ctt,_) =
1.6 (rewrite_inst thy' "tless_true" "erls" false [("bdv","s")] thm ct);
1.7 -if ctt = "0" then () else raise error "diff.sml: thm 'diff_const' diff.behav.";
1.8 +if ctt = "0" then () else error "diff.sml: thm 'diff_const' diff.behav.";
1.9 trace_rewrite := false;
1.10 "----- for 'd_d s a' we had 'a is_const' --> False --------^^^-----";
1.11
1.12 @@ -171,11 +171,11 @@
1.13 val (ct,_) = the (rewrite_inst thy' "tless_true" "erls" true
1.14 [("bdv","x::real")] thm ct);
1.15 if ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
1.16 -else raise error "diff.sml diff.behav. in rewrite 1";
1.17 +else error "diff.sml diff.behav. in rewrite 1";
1.18 "--- 7 ---";
1.19 val rls = ("Test_simplify");
1.20 val (ct,_) = the (rewrite_set thy' false rls ct);
1.21 -if ct="3 + 2 * x" then () else raise error "new behaviour in test-example";
1.22 +if ct="3 + 2 * x" then () else error "new behaviour in test-example";
1.23
1.24 val ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
1.25 val (ct,_) = the (rewrite_set thy' true rls ct);
1.26 @@ -249,7 +249,7 @@
1.27 (*val nxt = ("Rewrite_Inst",Rewrite_Inst (["(bdv,x)"],("diff_var","")));*)
1.28 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.29 if f2str f = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
1.30 -else raise error "diff.sml: diff.behav. in d_d x ^^^ 2 + 3 * x + 4";
1.31 +else error "diff.sml: diff.behav. in d_d x ^^^ 2 + 3 * x + 4";
1.32 "--- 7 ---";
1.33 (*------------------------------11.3.03--------------------
1.34 trace_rewrite:=true;
1.35 @@ -291,8 +291,8 @@
1.36 (*val nxt = ("End_Proof'",End_Proof');*)
1.37 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.38 if nxt = ("End_Proof'",End_Proof') andalso f2str f = "3 + 2 * x" then ()
1.39 -else raise error "diff.sml: new.behav. in me (*+ tacs input*)";
1.40 -(*if f = EmptyMout then () else raise error "new behaviour in + tacs input";
1.41 +else error "diff.sml: new.behav. in me (*+ tacs input*)";
1.42 +(*if f = EmptyMout then () else error "new behaviour in + tacs input";
1.43 meNEW extracts Form once more*)
1.44
1.45
1.46 @@ -464,7 +464,7 @@
1.47 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.48 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.49 if nxt = ("End_Proof'",End_Proof') then ()
1.50 -else raise error "new behaviour in tests/differentiate, 1.5.02 me from script";
1.51 +else error "new behaviour in tests/differentiate, 1.5.02 me from script";
1.52
1.53 "----------- primed id -------------------------------------------";
1.54 "----------- primed id -------------------------------------------";
1.55 @@ -483,7 +483,7 @@
1.56
1.57 val SOME (f'_,_) = rewrite_set_ Isac.thy false srls_diff screxp1;
1.58 if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then ()
1.59 -else raise error "diff.sml: diff.behav. in 'primed'";
1.60 +else error "diff.sml: diff.behav. in 'primed'";
1.61 atomty f'_;
1.62
1.63 val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \
1.64 @@ -525,15 +525,15 @@
1.65
1.66 val t = str2term "2/x^^^2";
1.67 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.68 -if term2str t = "2 * x ^^^ -2" then () else raise error "diff.sml 1/x";
1.69 +if term2str t = "2 * x ^^^ -2" then () else error "diff.sml 1/x";
1.70
1.71 val t = str2term "sqrt (x^^^3)";
1.72 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.73 -if term2str t = "x ^^^ (3 / 2)" then () else raise error "diff.sml x^1/2";
1.74 +if term2str t = "x ^^^ (3 / 2)" then () else error "diff.sml x^1/2";
1.75
1.76 val t = str2term "2 / sqrt x^^^3";
1.77 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.78 -if term2str t = "2 * x ^^^ (-3 / 2)" then () else raise error"diff.sml x^-1/2";
1.79 +if term2str t = "2 * x ^^^ (-3 / 2)" then () else error"diff.sml x^-1/2";
1.80 (* trace_rewrite := true;
1.81 trace_rewrite := false;
1.82 *)
1.83 @@ -541,16 +541,16 @@
1.84
1.85 val t = str2term "2 * x ^^^ -2";
1.86 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.87 -if term2str t = "2 / x ^^^ 2" then () else raise error "diff.sml sym 1/x";
1.88 +if term2str t = "2 / x ^^^ 2" then () else error "diff.sml sym 1/x";
1.89
1.90
1.91 val t = str2term "x ^^^ (3 / 2)";
1.92 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.93 -if term2str t = "sqrt (x ^^^ 3)" then () else raise error"diff.sml sym x^1/x";
1.94 +if term2str t = "sqrt (x ^^^ 3)" then () else error"diff.sml sym x^1/x";
1.95
1.96 val t = str2term "2 * x ^^^ (-3 / 2)";
1.97 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.98 -if term2str t ="2 / sqrt (x ^^^ 3)"then()else raise error"diff.sml sym x^-1/x";
1.99 +if term2str t ="2 / sqrt (x ^^^ 3)"then()else error"diff.sml sym x^-1/x";
1.100
1.101
1.102 (* trace_rewrite:=true;
1.103 @@ -576,7 +576,7 @@
1.104 val ((pt,p),_) = get_calc 1; show_pt pt;
1.105 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
1.106 "1 + 2 * x + -1 / x ^^^ 2 + -4 / x ^^^ 3" then ()
1.107 -else raise error "diff.sml: differentiate_on_R 2/x^2 changed";
1.108 +else error "diff.sml: differentiate_on_R 2/x^2 changed";
1.109
1.110 "-----------------------------------------------------------------";
1.111 states:=[];
1.112 @@ -598,7 +598,7 @@
1.113
1.114 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
1.115 "8 * x ^^^ 7" then ()
1.116 -else raise error "diff.sml: differentiate_on_R (x^3 * x^5) changed";
1.117 +else error "diff.sml: differentiate_on_R (x^3 * x^5) changed";
1.118
1.119
1.120 "----------- autoCalculate diff after_simplification -------------";
1.121 @@ -621,7 +621,7 @@
1.122 *)
1.123 val ((pt,p),_) = get_calc 1; show_pt pt;
1.124 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "8 * x ^^^ 7"
1.125 -then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed";
1.126 +then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
1.127
1.128 "-----------------------------------------------------------------";
1.129 states:=[];
1.130 @@ -635,7 +635,7 @@
1.131 autoCalculate 1 CompleteCalc;
1.132 val ((pt,p),_) = get_calc 1; show_pt pt;
1.133 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "15 * x ^^^ 14"
1.134 -then () else raise error "biegelinie.sml: 1st biegelin.7.27 changed";
1.135 +then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
1.136
1.137
1.138
1.139 @@ -689,4 +689,4 @@
1.140 appendFormula 1 "2*x + d_d x x + d_d x 1";
1.141 val ((pt,p),_) = get_calc 1; show_pt pt;
1.142 if existpt' ([3], Res) pt then ()
1.143 -else raise error "diff.sml: inform d_d x (x^2 + x + 1) doesnt work";
1.144 +else error "diff.sml: inform d_d x (x^2 + x + 1) doesnt work";