1.1 --- a/test/Tools/isac/Knowledge/rlang.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rlang.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -79,7 +79,7 @@
1.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.6 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
1.7 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 5 [x = 2]";
1.8 + | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 5 [x = 2]";
1.9
1.10 (*----------------- Schalk I s.86 Bsp 19 ------------------------*)
1.11 "Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";
1.12 @@ -109,7 +109,7 @@
1.13 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.14 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.15 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8]")) => ()
1.16 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 19 [x = 8]";
1.17 + | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 19 [x = 8]";
1.18
1.19 (*----------------- Schalk I s.86 Bsp 23 ------------------------*)
1.20 "Schalk I s.86 Bsp 19 ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))";
1.21 @@ -139,7 +139,7 @@
1.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.24 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -9]")) => ()
1.25 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 23 [x = -9]";
1.26 + | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 23 [x = -9]";
1.27
1.28 (*----------------- Schalk I s.86 Bsp 25 ------------------------*)
1.29 "Schalk I s.86 Bsp 25 ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)";
1.30 @@ -169,7 +169,7 @@
1.31 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.32 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.33 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -6 / 5]")) => ()
1.34 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 25 [x = -6 / 5]";
1.35 + | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 25 [x = -6 / 5]";
1.36
1.37 (*----------------- Schalk I s.86 Bsp 28b ------------------------*)
1.38 "Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";
1.39 @@ -197,7 +197,7 @@
1.40 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.41 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
1.42 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
1.43 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 28b []";
1.44 + | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 28b []";
1.45
1.46 (*WN---v *)
1.47 val bdv= (term_of o the o (parse thy)) "bdv";
1.48 @@ -205,12 +205,12 @@
1.49 val t = (term_of o the o (parse thy)) "3 * x / 5";
1.50 val SOME (t',_) = rewrite_set_inst_ PolyEq.thy true
1.51 [(bdv, v)] make_ratpoly_in t;
1.52 -if term2str t' = "3 / 5 * x" then () else raise error "rlang.sml: 1";
1.53 +if term2str t' = "3 / 5 * x" then () else error "rlang.sml: 1";
1.54
1.55 val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
1.56 val subst = [(str2term "bdv", str2term "x")];
1.57 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1.58 -if term2str t' = "1 / 18 = 0" then () else raise error "rlang.sml: 2";
1.59 +if term2str t' = "1 / 18 = 0" then () else error "rlang.sml: 2";
1.60 (*WN---^ *)
1.61
1.62 (*----------------- Schalk I s.87 Bsp 36b ------------------------*)
1.63 @@ -240,7 +240,7 @@
1.64 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.65 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.66 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -237 / 65]")) => ()
1.67 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 36b [x = -237 / 65]";
1.68 + | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 36b [x = -237 / 65]";
1.69
1.70
1.71 (*WN---v *)
1.72 @@ -249,7 +249,7 @@
1.73 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1.74 term2str t';
1.75 if term2str t' = "79 / 12 + 65 / 36 * x = 0" then ()
1.76 -else raise error "rlang.sml: 3";
1.77 +else error "rlang.sml: 3";
1.78 (*WN---^ *)
1.79
1.80
1.81 @@ -279,7 +279,7 @@
1.82 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.83 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.84 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "296 + -3900 * x = 0")) then ()
1.85 -else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 38b";
1.86 +else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 38b";
1.87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.90 @@ -291,7 +291,7 @@
1.91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.93 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 74 / 975]")) => ()
1.94 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 38b [x = 74 / 975]";
1.95 + | _ => error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 38b [x = 74 / 975]";
1.96
1.97 (*----------------- Schalk I s.87 Bsp 40b ------------------------*)
1.98 "Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";
1.99 @@ -321,7 +321,7 @@
1.100 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;*)
1.102 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "15 + -5 * x = 0")) then ()
1.103 -else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b";
1.104 +else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b";
1.105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.108 @@ -332,7 +332,7 @@
1.109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.111 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 3]")) => ()
1.112 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b [x = 3]";
1.113 + | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b [x = 3]";
1.114
1.115
1.116 (*----------------- Schalk I s.87 Bsp 44a ------------------------*)
1.117 @@ -365,20 +365,20 @@
1.118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.120 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1]")) => ()
1.121 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 44a [x = 1]";
1.122 + | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 44a [x = 1]";
1.123
1.124 (*WN---v *)
1.125 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
1.126 val subst = [(str2term "bdv", str2term "x")];
1.127 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1.128 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
1.129 -else raise error "rlang.sml: 4";
1.130 +else error "rlang.sml: 4";
1.131
1.132 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 + (6*x)^^^2 - 29";
1.133 val subst = [(str2term "bdv", str2term "x")];
1.134 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1.135 if term2str t' = "-35 + 35 * x" then ()
1.136 -else raise error "rlang.sml: 4.1";
1.137 +else error "rlang.sml: 4.1";
1.138 (*WN---^ *)
1.139
1.140 (*----------------- Schalk I s.87 Bsp 52a ------------------------*)
1.141 @@ -404,7 +404,7 @@
1.142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.143 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.144 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "16 + 12 * x = 0")) then ()
1.145 -else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 52a";
1.146 +else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 52a";
1.147 (*Subproblem["degree_1", "polynomial", "univariate", "equation"]*)
1.148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.150 @@ -416,7 +416,7 @@
1.151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.152 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.153 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -4 / 3]")) => ()
1.154 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 52a [x = -4 / 3]";
1.155 + | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 52a [x = -4 / 3]";
1.156
1.157 (*----------------- Schalk I s.87 Bsp 55b ------------------------*)
1.158 "Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
1.159 @@ -447,7 +447,7 @@
1.160 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 040209 MGs norm_Rational*)
1.161 (* val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"])*)
1.162 if f= Form' (FormKF (~1, EdUndef, 0, Nundef, "-6 * x + 5 * x ^^^ 2 = 0"))then()
1.163 -else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
1.164 +else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b";
1.165 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.166 (*nxt=Model_Problem["bdv_only","degree_2","polynomial","univariate","equation*)
1.167 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.168 @@ -477,11 +477,11 @@
1.169 val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
1.170 val [(aaa,ppp)] = get_assumptions_ pt p;
1.171 if term2str aaa = "9 * x + -6 * x ^^^ 2 + x ^^^ 3 ~= 0" then ()
1.172 -else raise error "rlang.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], asms";
1.173 +else error "rlang.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], asms";
1.174 (*WN060717 unintentionally changed some rls/ord while
1.175 completing knowl. for thes2file...
1.176 if term2str aaa = "9 * x + (x ^^^ 3 + -6 * x ^^^ 2) ~= 0" then ()
1.177 -else raise error "rlang.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], asms";
1.178 +else error "rlang.sml: diff.behav. in I s.87 Bsp 55b [x = 6 / 5], asms";
1.179 .... but it became even better*)
1.180
1.181 (*22.10.03:
1.182 @@ -502,7 +502,7 @@
1.183 val nxt =Check_Postcond ["rational","univariate","equation"]) *)
1.184 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.185 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 6 / 5]")) => ()
1.186 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1.187 + | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
1.188
1.189 (*----------------- Schalk I s.88 Bsp 64c ------------------------*)
1.190 "Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";
1.191 @@ -530,7 +530,7 @@
1.192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
1.194 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-3 + -1 * x = 0")) then ()
1.195 -else raise error "rlangsml: diff.behav. in Schalk I s.88 Bsp 64c";
1.196 +else error "rlangsml: diff.behav. in Schalk I s.88 Bsp 64c";
1.197 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.199 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.200 @@ -542,7 +542,7 @@
1.201 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.202 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.203 case f of Form' (FormKF (_,_,0,_,"[x = -3]")) => ()
1.204 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.88 Bsp 64c [x = -3]";
1.205 + | _ => error "rlang.sml: diff.behav. in Schalk I s.88 Bsp 64c [x = -3]";
1.206
1.207 (*----------------- Schalk I s.88 Bsp 79a (2) ------------------------*)
1.208 "Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";
1.209 @@ -571,7 +571,7 @@
1.210 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.211 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.212 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[m1 = -1 * m2 * v2 / v1]")) => ()
1.213 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.88 Bsp 79a (2) [m1 = -1 * m2 * v2 / v1]";
1.214 + | _ => error "rlang.sml: diff.behav. in Schalk I s.88 Bsp 79a (2) [m1 = -1 * m2 * v2 / v1]";
1.215
1.216 (*----------------- Schalk I s.89 Bsp 90a(1) ------------------------*)
1.217 "Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";
1.218 @@ -613,7 +613,7 @@
1.219 0,
1.220 Nundef,
1.221 "f * w + -1 * u * v0 + -1 * v0 * w + f * v = 0")) then ()
1.222 -else raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a";
1.223 +else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a";
1.224 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.225 (*val nxt = Model_Problem ["degree_1","polynomial","univariate","equation"])*)
1.226 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.227 @@ -646,10 +646,10 @@
1.228 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.229 case f of Form' (FormKF (~1,EdUndef,0,Nundef,
1.230 "[v = (u * v0 + v0 * w + -1 * f * w) / f]")) => ()
1.231 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (1) [v=...]";
1.232 + | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (1) [v=...]";
1.233 if get_assumptions_ pt p =
1.234 [(str2term"(u * v0 + v0 * w + -1 * f * w) / f + w ~= 0",[])] then ()
1.235 -else raise error "rlang.sml: diff.behav. in I s.89 Bsp 90a (1) [v=...] asm";
1.236 +else error "rlang.sml: diff.behav. in I s.89 Bsp 90a (1) [v=...] asm";
1.237
1.238
1.239 (*----------------- Schalk I s.89 Bsp 90a(2) ------------------------*)
1.240 @@ -682,7 +682,7 @@
1.241 0,
1.242 Nundef,
1.243 "f * v + -1 * u * v0 + (f + -1 * v0) * w = 0")) then ()
1.244 -else raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (2)";
1.245 +else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (2)";
1.246 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.247 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.248 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.249 @@ -693,12 +693,12 @@
1.250 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.251 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.252 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[w = (u * v0 + -1 * f * v) / (f + -1 * v0)]")) => ()
1.253 - | _ => raise error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2)";
1.254 + | _ => error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2)";
1.255 if get_assumptions_ pt p =
1.256 [(str2term"v + (u * v0 + -1 * f * v) / (f + -1 * v0) ~= 0",[]),
1.257 (str2term"f + -1 * v0 ~= 0",[])]
1.258 then writeln "asm should be simplified ???"
1.259 -else raise error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2) asm";
1.260 +else error "rlang.sml: diff.behav. in Schalk I Bsp 90a(2) asm";
1.261
1.262 (*----------------- Schalk I s.89 Bsp 98a(1) ------------------------*)
1.263 "Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";
1.264 @@ -727,7 +727,7 @@
1.265 if f = Form'
1.266 (FormKF
1.267 (~1, EdUndef, 0, Nundef, "-1 * R * R2 + (R2 + -1 * R) * R1 = 0"))then()
1.268 -else raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 98a (1)";
1.269 +else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 98a (1)";
1.270 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.271 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.272 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.273 @@ -738,12 +738,12 @@
1.274 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.275 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.276 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + -1 * R)]")) => ()
1.277 - | _ => raise error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]";
1.278 + | _ => error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]";
1.279 if get_assumptions_ pt p = [(str2term"R * R2 * R2 ~= (R2 + -1 * R) * 0",[]),
1.280 (str2term"R2 + -1 * R ~= 0",[]),
1.281 (str2term"R2 + -1 * R ~= 0",[])]
1.282 then writeln "asm should be simplified"
1.283 -else raise error "rlang.sml: diff.behav. in 98a(1) asm";
1.284 +else error "rlang.sml: diff.behav. in 98a(1) asm";
1.285
1.286 (*----------------- Schalk I s.89 Bsp 104a(1) ------------------------*)
1.287 "Schalk I s.89 Bsp 104a (1) (y^^^2=2*p*x)";
1.288 @@ -772,10 +772,10 @@
1.289 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.290 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.291 case f of Form' (FormKF (_,_,0,_,"[p = y ^^^ 2 / (2 * x)]")) => ()
1.292 - | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a (1) [p = y^2/(2*x)]";
1.293 + | _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a (1) [p = y^2/(2*x)]";
1.294 if get_assumptions_ pt p = [(str2term"-2 * x ~= 0",[])]
1.295 then writeln"should be x ~= 0\nshould be x ~= 0\nshould be x ~= 0\n"
1.296 -else raise error "rlang.sml: diff.behav. in I s.89 Bsp 104a(1) asm";
1.297 +else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(1) asm";
1.298
1.299
1.300 (*----------------- Schalk I s.89 Bsp 104a(2) ------------------------*)
1.301 @@ -806,9 +806,9 @@
1.302 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.303 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.304 case f of Form' (FormKF (_,_,0,_,"[y = sqrt (2 * p * x), y = -1 * sqrt (2 * p * x)]")) => ()
1.305 -| _ => raise error "rlang.sml: diff.behav. Schalk I s.89 Bsp 104a(2) [x = ]";
1.306 +| _ => error "rlang.sml: diff.behav. Schalk I s.89 Bsp 104a(2) [x = ]";
1.307 if get_assumptions_ pt p = [(str2term"0 <= -1 * (-2 * p * x)",[]),(str2term"0 <= -1 * (-2 * p * x)",[])] then writeln "asm should be simplified\nshould be simplified"
1.308 -else raise error "rlang.sml: diff.behav. in I s.89 Bsp 104a(2) asm";
1.309 +else error "rlang.sml: diff.behav. in I s.89 Bsp 104a(2) asm";
1.310
1.311
1.312 (*----------------- Schalk I s.90 Bsp 118a (1) ------------------------*)
1.313 @@ -852,14 +852,14 @@
1.314 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_asm (fst p, fst p) pt;
1.315 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;f2str f;get_asm (fst p, fst p) pt;
1.316 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = sqrt ((a ^^^ 2 * b ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2) / b ^^^ 2),\n x = -1 * sqrt ((a ^^^ 2 * b ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2) / b ^^^ 2)]")) => writeln"should be simplified MG"
1.317 -| _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) [x = ]";
1.318 +| _ => error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) [x = ]";
1.319 val asms = get_assumptions_ pt p;
1.320 if asms = [(str2term"0 * b ^^^ 2 <= -1 * (a ^^^ 2 * y ^^^ 2 + -1 * a ^^^ 2 * b ^^^ 2)", []),
1.321 (str2term"b ^^^ 2 ~= 0", []),
1.322 (str2term"0 * b ^^^ 2 <= -1 * (a ^^^ 2 * y ^^^ 2 + -1 * a ^^^ 2 * b ^^^ 2)", []),
1.323 (str2term"b ^^^ 2 ~= 0", [])
1.324 ] then writeln"should be simplified MG"
1.325 -else raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) asms";
1.326 +else error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) asms";
1.327
1.328 (*----------------- Schalk I s.102 Bsp 268(1) ------------------------*)
1.329 "Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2-y3)+x2*(y3 - y1)+x3*(y1 - y2)))";
1.330 @@ -889,9 +889,9 @@
1.331 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.332 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.333 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x2 =\n (-2 * A + x1 * y2 + x3 * y1 + -1 * x1 * y3 + -1 * x3 * y2) /\n (y1 + -1 * y3)]")) => ()
1.334 -| _ => raise error "rlang.sml: diff.behav. Schalk I s.102 Bsp 268(1) [x2=...]";
1.335 +| _ => error "rlang.sml: diff.behav. Schalk I s.102 Bsp 268(1) [x2=...]";
1.336 if get_assumptions_ pt p = [(str2term"y1 / 2 + -1 * y3 / 2 ~= 0",[])] then ()
1.337 -else raise error "rlang.sml: diff.behav. in I s.102 Bsp 268(1) asm";
1.338 +else error "rlang.sml: diff.behav. in I s.102 Bsp 268(1) asm";
1.339
1.340 (*-------------------- Schalk II ----------------------------*)
1.341 (*-------------------- Schalk II ----------------------------*)
1.342 @@ -926,7 +926,7 @@
1.343 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.344 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
1.345 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-2 + x = 0")) then ()
1.346 -else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 67b";
1.347 +else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 67b";
1.348 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.349 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.350 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.351 @@ -937,7 +937,7 @@
1.352 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.353 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.354 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
1.355 - | _ => raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 67b [x=2]";
1.356 + | _ => error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 67b [x=2]";
1.357
1.358 (*----------------- Schalk II s.56 Bsp 68a ------------------------*)
1.359 "Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
1.360 @@ -983,7 +983,7 @@
1.361 if f = Form'
1.362 (FormKF
1.363 (~1, EdUndef, 0, Nundef, "256 + -2368 * x + 576 * x ^^^ 2 = 0"))then()
1.364 -else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 68a";
1.365 +else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 68a";
1.366 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.367 get_assumptions_ pt p;
1.368 (* val nxt = ("Model_Problem", Model_Problem
1.369 @@ -1001,7 +1001,7 @@
1.370 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.371 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4, x = 1 / 9]"))
1.372 then writeln "only [x = 4] !\nonly [x = 4] !\nonly [x = 4] !\n"
1.373 -else raise error "rlang.sml: diff.behav. in II 68a";
1.374 +else error "rlang.sml: diff.behav. in II 68a";
1.375 val asms = get_assumptions_ pt p;
1.376 if asms2str asms =
1.377 "[(0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56, []),\
1.378 @@ -1019,7 +1019,7 @@
1.379 (str2term"9 ~= 0", []),
1.380 (str2term"0 <= (25 * (1 / 9) + -1 * (16 + 49 * (1 / 9))) * -56", [])]*)
1.381 then "should get True * False!!!"
1.382 -else raise error "rlang.sml: diff.behav. in II 68a asms";
1.383 +else error "rlang.sml: diff.behav. in II 68a asms";
1.384
1.385 (*----------------- Schalk II s.56 Bsp 73b ------------------------*)
1.386 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
1.387 @@ -1056,7 +1056,7 @@
1.388 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.389 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.390 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
1.391 -else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 73b";
1.392 +else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 73b";
1.393 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.394 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.395 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.396 @@ -1069,7 +1069,7 @@
1.397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.398 val asm = get_assumptions_ pt p;
1.399 if asm=[] andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso nxt = ("End_Proof'",End_Proof') then ()
1.400 -else raise error "rlang.sml: diff.behav. in UniversalList 2";
1.401 +else error "rlang.sml: diff.behav. in UniversalList 2";
1.402
1.403 (*----------------- Schalk II s.56 Bsp 74a ------------------------*)
1.404 "Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";
1.405 @@ -1107,7 +1107,7 @@
1.406 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.407 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.408 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + 4 * x = 0")) then ()
1.409 -else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a";
1.410 +else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a";
1.411 (*-> ubproblem ("PolyEq", ["degree_1", ...]*)
1.412 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.413 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.414 @@ -1120,7 +1120,7 @@
1.415 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.416 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.417 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 6]")) => ()
1.418 - | _ => raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a [x = 6]";
1.419 + | _ => error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 74a [x = 6]";
1.420
1.421
1.422 (*----------------- Schalk II s.56 Bsp 77b ------------------------*)
1.423 @@ -1167,7 +1167,7 @@
1.424 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.425 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; since MGs norm_Rational*)
1.426 if f = Form'(FormKF (~1, EdUndef, 0, Nundef, "451584 + -112896 * x = 0"))then()
1.427 -else raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 77b";
1.428 +else error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 77b";
1.429 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.430 (* val nxt = ("Model_Problem",
1.431 Model_Problem ["degree_1","polynomial","univariate","equation"])*)
1.432 @@ -1181,7 +1181,7 @@
1.433 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.434 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.435 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
1.436 - | _ => raise error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 77b []";
1.437 + | _ => error "rlang.sml: diff.behav. in Schalk II s.56 Bsp 77b []";
1.438 (*added 040209 at introducing MGs norm_Rational ?!*)
1.439 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.440
1.441 @@ -1214,7 +1214,7 @@
1.442 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.443 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.444 case f of Form' (FormKF (_,_,0,_,"[x = 5, x = -5]")) => ()
1.445 - | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 4 []";
1.446 + | _ => error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 4 []";
1.447
1.448
1.449 (*----------------- Schalk II s.66 Bsp 8a ------------------------*)
1.450 @@ -1242,7 +1242,7 @@
1.451 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.452 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.453 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-8 + 2 * x ^^^ 2 = 0")) then ()
1.454 -else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a";
1.455 +else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a";
1.456 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
1.457 (*
1.458 val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;
1.459 @@ -1257,7 +1257,7 @@
1.460 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.461 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.462 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.463 - | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a [x = 2, x = -2]";
1.464 + | _ => error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a [x = 2, x = -2]";
1.465
1.466 (*----------------- Schalk II s.66 Bsp 10b ------------------------*)
1.467 "Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
1.468 @@ -1290,7 +1290,7 @@
1.469 0,
1.470 Nundef,
1.471 "60 + 28 * x + -13 * x ^^^ 2 + -1 * x ^^^ 3 = 0")) then ()
1.472 -else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 10b";
1.473 +else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 10b";
1.474 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.475 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.476 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.477 @@ -1332,7 +1332,7 @@
1.478 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.479 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.480 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-25 + x ^^^ 2 = 0")) then ()
1.481 -else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 20a";
1.482 +else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 20a";
1.483 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.484 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.485 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.486 @@ -1345,7 +1345,7 @@
1.487 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.488 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.489 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 5, x = -5]")) => ()
1.490 - | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 20a [x = 5, x = -5]";
1.491 + | _ => error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 20a [x = 5, x = -5]";
1.492
1.493 (*----------------- Schalk II s.66 Bsp 23b ------------------------*)
1.494 "Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";
1.495 @@ -1384,7 +1384,7 @@
1.496 if f = Form'
1.497 (FormKF
1.498 (~1, EdUndef, 0, Nundef, "-1064944 + 32 * x + -48 * x ^^^ 2 = 0"))then()
1.499 -else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 23b";
1.500 +else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 23b";
1.501 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.502 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.503 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.504 @@ -1393,7 +1393,7 @@
1.505 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.506 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.507 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[]")) => ()
1.508 - | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 23b []";
1.509 + | _ => error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 23b []";
1.510
1.511 (*----------------- Schalk II s.66 Bsp 28a ------------------------*)
1.512 "Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";
1.513 @@ -1427,7 +1427,7 @@
1.514 "c ^^^ 4 / d ^^^ 2 + A ^^^ 2 * d ^^^ 2 / d ^^^ 2 +\n-4 * c ^^^ 2 / d ^^^ 2 * a ^^^ 2 =\n0")) then ()*)
1.515 if f2str f =
1.516 "c ^^^ 4 / d ^^^ 2 + A ^^^ 2 / 1 + -4 * c ^^^ 2 / d ^^^ 2 * a ^^^ 2 = 0"
1.517 -then () else raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a";
1.518 +then () else error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a";
1.519 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.520 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.521 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.522 @@ -1438,7 +1438,7 @@
1.523 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.524 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.525 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[a = sqrt ((c ^^^ 4 + A ^^^ 2 * d ^^^ 2) / (4 * c ^^^ 2)),\n a = -1 * sqrt ((c ^^^ 4 + A ^^^ 2 * d ^^^ 2) / (4 * c ^^^ 2))]")) => ()
1.526 -| _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a [a=...]";
1.527 +| _ => error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 28a [a=...]";
1.528
1.529
1.530
1.531 @@ -1479,7 +1479,7 @@
1.532 0,
1.533 Nundef,
1.534 "b * a ^^^ 2 + -1 * a * b ^^^ 2 + (a ^^^ 2 + b ^^^ 2 + -2 * a * b) * x +\n(b + -1 * a) * x ^^^ 2 =\n0")) then ()
1.535 -else raise error "rlang.sml: diff.behav. in chalk I s.87 Bsp 38b";
1.536 +else error "rlang.sml: diff.behav. in chalk I s.87 Bsp 38b";
1.537 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.538 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.539 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.540 @@ -1502,7 +1502,7 @@
1.541 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;(*1 additional for MGs norm_Rational*)
1.542 if p = ([],Res) andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,
1.543 "[x =\n (2 * a * b + -1 * a ^^^ 2 + -1 * b ^^^ 2 +\n sqrt\n (a ^^^ 4 + b ^^^ 4 + -4 * a * a * b ^^^ 2 + -4 * a * b * a ^^^ 2 +\n -4 * b * b * a ^^^ 2 +\n 4 * a * a * b ^^^ 2 +\n 4 * a * b * a ^^^ 2 +\n 2 * a ^^^ 2 * b ^^^ 2)) /\n (-2 * a + 2 * b),\n x =\n (2 * a * b + -1 * a ^^^ 2 + -1 * b ^^^ 2 +\n -1 *\n sqrt\n (a ^^^ 4 + b ^^^ 4 + -4 * a * a * b ^^^ 2 + -4 * a * b * a ^^^ 2 +\n -4 * b * b * a ^^^ 2 +\n 4 * a * a * b ^^^ 2 +\n 4 * a * b * a ^^^ 2 +\n 2 * a ^^^ 2 * b ^^^ 2)) /\n (-2 * a + 2 * b)]")) andalso nxt = ("End_Proof'",End_Proof') then writeln"simplify MG"
1.544 -else raise error "rlang.sml: diff.behav. in rational-a-b";
1.545 +else error "rlang.sml: diff.behav. in rational-a-b";
1.546
1.547 (*----------------- Schalk II s.68 Bsp 56a ------------------------*)
1.548 "Schalk II s.68 Bsp 56a ((a+b*x)/(a-b*x) - (a - b*x)/(a+b*x)= (4*a*b)/(a^^^2 - b^^^2))";
1.549 @@ -1629,7 +1629,7 @@
1.550 Nundef,
1.551 (*"-4 * b ^^^ 2 + -4 * a * b + 4 * b ^^^ 2 + 8 * a * b +\n(-2 * a + -4 * a + -4 * b + 2 * a + 8 * b) * x +\n-4 * x ^^^ 2 =\n0" before MG*)
1.552 "4 * a * b + (-4 * a + 4 * b) * x + -4 * x ^^^ 2 = 0")) then ()
1.553 -else raise error "rlang.sml: diff.behav. in Schalk II s.68 Bsp 61b";
1.554 +else error "rlang.sml: diff.behav. in Schalk II s.68 Bsp 61b";
1.555 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.556 (*val nxt = ("Model_Problem", Model_Problem
1.557 ["abcFormula","degree_2","polynomial","univariate","equation"])*)
1.558 @@ -1649,7 +1649,7 @@
1.559 (*if f = Form' (FormKF (~1,EdUndef,0,Nundef, with norm_Rational before MG
1.560 "[x =\n (-2 * a + -4 * b + 6 * a +\n sqrt\n (32 * a * b + -16 * a ^^^ 2 + -48 * b ^^^ 2 + 24 * a ^^^ 2 +\n 64 * b ^^^ 2 +\n 8 * a ^^^ 2)) /\n -8,\n x =\n (-2 * a + -4 * b + 6 * a +\n -1 *\n sqrt\n (32 * a * b + -16 * a ^^^ 2 + -48 * b ^^^ 2 + 24 * a ^^^ 2 +\n 64 * b ^^^ 2 +\n 8 * a ^^^ 2)) /\n -8]")) then writeln"simplify MG"*)
1.561 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x =\n (-4 * b + 4 * a + sqrt (32 * a * b + 16 * a ^^^ 2 + 16 * b ^^^ 2)) / -8,\n x =\n (-4 * b + 4 * a + -1 * sqrt (32 * a * b + 16 * a ^^^ 2 + 16 * b ^^^ 2)) /\n -8]")) then ()
1.562 -else raise error "rlang.sml: diff.behav. Bsp 61b";
1.563 +else error "rlang.sml: diff.behav. Bsp 61b";
1.564 (*WN.18.12.03: extreme run-time !!!*)
1.565
1.566
1.567 @@ -1681,7 +1681,7 @@
1.568 0,
1.569 Nundef,
1.570 "-4 * a * b + (-4 * b + 2 * a) * x + 2 * x ^^^ 2 = 0")) then ()
1.571 -else raise error "rlang.sml: diff.behav. in Schalk II s.68 Bsp 62b";
1.572 +else error "rlang.sml: diff.behav. in Schalk II s.68 Bsp 62b";
1.573 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.574 (*val nxt = ("Model_Problem", Model_Problem
1.575 ["abcFormula","degree_2","polynomial","univariate","equation"])*)
1.576 @@ -1699,7 +1699,7 @@
1.577 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;introduc.MGs norm_Rational*)
1.578 if f = Form' (FormKF (~1,EdUndef,0,Nundef,
1.579 "[x = (-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4,\n x =\n (-2 * a + 4 * b + -1 * sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4]")) then writeln "simplify MG"
1.580 -else raise error "rlang.sml: diff.behav. in II 62b [x=...]";
1.581 +else error "rlang.sml: diff.behav. in II 62b [x=...]";
1.582 val asms = get_assumptions_ pt p;
1.583 if asms = [(str2term"0 <= ((-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 + a) ^^^ 2 + ((-2 * a + 4 * b + sqrt (16 * a * b + 16 * b ^^^ 2 + 4 * a ^^^ 2)) / 4 - 2 * b) ^^^ 2", []),
1.584 (str2term"0 <= a + 2 * b", []),
1.585 @@ -1710,7 +1710,7 @@
1.586 (str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2", []),
1.587 (str2term"8 * (-4 * a * b) <= (-4 * b + 2 * a) ^^^ 2", [])]
1.588 then writeln "should be simplified MG"
1.589 -else raise error "rlang.sml: diff.behav. in II 62b asms";
1.590 +else error "rlang.sml: diff.behav. in II 62b asms";
1.591
1.592 "------ WN.TEST---------------------------------";
1.593 "------ WN.TEST---------------------------------";
1.594 @@ -1732,7 +1732,7 @@
1.595 val subst = [(str2term "bdv", str2term "x")];
1.596 val SOME (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
1.597 if term2str t' = "x ^^^ 2 + 2 * x ^^^ 3 = 0" then ()
1.598 -else raise error "rlang.sml: 7";
1.599 +else error "rlang.sml: 7";
1.600 *)
1.601 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.602 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.603 @@ -1746,7 +1746,7 @@
1.604 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.605 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.606 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = 0, x = -1 / 2]")) then()
1.607 -else raise error "rlang.sml WN.TEST new behaviour";
1.608 +else error "rlang.sml WN.TEST new behaviour";
1.609
1.610 "------ rlang.sml end---------------------------------";
1.611
1.612 @@ -1798,7 +1798,7 @@
1.613 if f = Form' (FormKF (~1,EdUndef,0,Nundef,
1.614 "[a = sqrt ((-1 * b ^^^ 2 + 4 * r ^^^ 2) / 1),\n a = -1 * sqrt ((-1 * b ^^^ 2 + 4 * r ^^^ 2) / 1)]")) andalso nxt = ("End_Proof'",End_Proof')
1.615 then writeln"simplify result\nsimplify result\nsimplify result"
1.616 -else raise error "rlang.sml: diff.behav. in Pythagoras";
1.617 +else error "rlang.sml: diff.behav. in Pythagoras";
1.618 val asms = get_assumptions_ pt p;
1.619 (*if asms = [(str2term"0 <= -4 * (b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)", []),
1.620 (str2term"0 <= -4 * (b ^^^ 2 / 4 + -4 * r ^^^ 2 / 4)", [])]*)
1.621 @@ -1806,7 +1806,7 @@
1.622 "[(0 <= -4 * (b ^^^ 2 / 4 + -1 * r ^^^ 2 / 1), []),\
1.623 \(0 <= -4 * (b ^^^ 2 / 4 + -1 * r ^^^ 2 / 1), [])]"
1.624 then writeln"simplify result\nsimplify result\nsimplify result"
1.625 -else raise error "rlang.sml: diff.behav. in Pythagoras asms";
1.626 +else error "rlang.sml: diff.behav. in Pythagoras asms";
1.627
1.628
1.629 "-------------------- WN.15.5.03: equation within the maximum example ------";
1.630 @@ -1864,7 +1864,7 @@
1.631 0,
1.632 Nundef,
1.633 "-16 * r ^^^ 4 + 8 * r ^^^ 2 * u ^^^ 2 = 0")) then ()
1.634 -else raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 38b";
1.635 +else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 38b";
1.636 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.637 (*val nxt = Model_Problem ["sq_only","degree_2","polynomial","univariate","equation"]) *)
1.638 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.639 @@ -1880,4 +1880,4 @@
1.640 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.641 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.642 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[u = sqrt (2 * r ^^^ 2 / 1), u = -1 * sqrt (2 * r ^^^ 2 / 1)]")) then()
1.643 -else raise error "rlang.sml WN.TEST new behaviour in max-rooteq";
1.644 +else error "rlang.sml WN.TEST new behaviour in max-rooteq";