1.1 --- a/test/Tools/isac/Knowledge/polyeq.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -41,60 +41,60 @@
1.4 val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
1.5 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t1;
1.6 if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
1.7 - else raise error "polyeq.sml: diff.behav. in lhs";
1.8 + else error "polyeq.sml: diff.behav. in lhs";
1.9
1.10
1.11 val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
1.12 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t2;
1.13 if (term2str t) = "True" then ()
1.14 - else raise error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.15 + else error "polyeq.sml: diff.behav. 1 in is_expended_in";
1.16
1.17 val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
1.18 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t0;
1.19 if (term2str t) = "False" then ()
1.20 - else raise error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.21 + else error "polyeq.sml: diff.behav. 2 in is_poly_in";
1.22
1.23
1.24 val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
1.25 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.26 if (term2str t) = "True" then ()
1.27 - else raise error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.28 + else error "polyeq.sml: diff.behav. 3 in is_poly_in";
1.29
1.30
1.31 val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
1.32 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
1.33 if (term2str t) = "True" then ()
1.34 - else raise error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.35 + else error "polyeq.sml: diff.behav. 4 in is_expended_in";
1.36
1.37
1.38 val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
1.39 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t6;
1.40 if (term2str t) = "True" then ()
1.41 - else raise error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.42 + else error "polyeq.sml: diff.behav. 5 in is_expended_in";
1.43
1.44 val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.45 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.46 if (term2str t) = "True" then ()
1.47 - else raise error "polyeq.sml: diff.behav. in has_degree_in_in";
1.48 + else error "polyeq.sml: diff.behav. in has_degree_in_in";
1.49
1.50
1.51 val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
1.52 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t3;
1.53 if (term2str t) = "False" then ()
1.54 - else raise error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.55 + else error "polyeq.sml: diff.behav. 6 in has_degree_in_in";
1.56
1.57 val t4 = (term_of o the o (parse thy))
1.58 "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
1.59 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t4;
1.60 if (term2str t) = "False" then ()
1.61 - else raise error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.62 + else error "polyeq.sml: diff.behav. 7 in has_degree_in_in";
1.63
1.64
1.65 val t5 = (term_of o the o (parse thy))
1.66 "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
1.67 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_prls t5;
1.68 if (term2str t) = "True" then ()
1.69 - else raise error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
1.70 + else error "polyeq.sml: diff.behav. 8 in has_degree_in_in";
1.71
1.72
1.73 "----------- test matching problems --------------------------0---";
1.74 @@ -138,7 +138,7 @@
1.75 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.76 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.77 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
1.78 - | _ => raise error "polyeq.sml: diff.behav. in 1 = 0 -> []";
1.79 + | _ => error "polyeq.sml: diff.behav. in 1 = 0 -> []";
1.80
1.81 "----- d0_true ------";
1.82 (*EP-7*)
1.83 @@ -156,7 +156,7 @@
1.84 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.85 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.86 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) => ()
1.87 - | _ => raise error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
1.88 + | _ => error "polyeq.sml: diff.behav. in 0 = 0 -> UniversalList";
1.89
1.90 "-------------------- test thm's degree_2 ------------------------------------------";
1.91 "-------------------- test thm's degree_2 ------------------------------------------";
1.92 @@ -189,7 +189,7 @@
1.93 ([5],Res) "[x = 2, x = -1]" Check_Postcond*)
1.94 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.95 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
1.96 - | _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
1.97 + | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
1.98
1.99 "----- d2_pqformula1_neg ------";
1.100 (*EP-8*)
1.101 @@ -213,7 +213,7 @@
1.102 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.103 val asm = get_assumptions_ pt p;
1.104 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) andalso asm = [] then ()
1.105 -else raise error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
1.106 +else error "polyeq.sml: diff.behav. in 2 +(-1)*x + x^^^2 = 0";
1.107
1.108 "----- d2_pqformula2 ------";
1.109 val fmz = ["equality (-2 +(-1)*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.110 @@ -232,7 +232,7 @@
1.111 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.112 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.113 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -1]")) => ()
1.114 - | _ => raise error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
1.115 + | _ => error "polyeq.sml: diff.behav. in -2 + (-1)*x + x^2 = 0 -> [x = 2, x = -1]";
1.116
1.117
1.118 "----- d2_pqformula2_neg ------";
1.119 @@ -273,7 +273,7 @@
1.120 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.121 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.122 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
1.123 - | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
1.124 + | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0-> [x = 1, x = -2]";
1.125
1.126 "----- d2_pqformula3_neg ------";
1.127 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.128 @@ -312,7 +312,7 @@
1.129 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.130 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.131 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
1.132 - | _ => raise error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
1.133 + | _ => error "polyeq.sml: diff.behav. in -2 + x + 1*x^^^2 = 0 -> [x = 1, x = -2]";
1.134
1.135 "----- d2_pqformula4_neg ------";
1.136 val fmz = ["equality ( 2 + x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.137 @@ -349,7 +349,7 @@
1.138 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.139 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.140 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.141 - | _ => raise error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
1.142 + | _ => error "polyeq.sml: diff.behav. in 1*x + x^2 = 0 -> [x = 0, x = -1]";
1.143
1.144 "----- d2_pqformula6 ------";
1.145 val fmz = ["equality (1*x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.146 @@ -368,7 +368,7 @@
1.147 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.148 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.149 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.150 - | _ => raise error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.151 + | _ => error "polyeq.sml: diff.behav. in 1*x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.152
1.153 "----- d2_pqformula7 ------";
1.154 (*EP-10*)
1.155 @@ -388,7 +388,7 @@
1.156 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.157 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.158 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.159 - | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.160 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.161
1.162 "----- d2_pqformula8 ------";
1.163 val fmz = ["equality ( x + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.164 @@ -408,7 +408,7 @@
1.165 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.166 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.167 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.168 - | _ => raise error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.169 + | _ => error "polyeq.sml: diff.behav. in x + 1*x^2 = 0 -> [x = 0, x = -1]";
1.170
1.171 "----- d2_pqformula9 ------";
1.172 val fmz = ["equality (-4 + x^^^2 = 0)", "solveFor x","solutions L"];
1.173 @@ -427,7 +427,7 @@
1.174 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.175 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.176 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.177 - | _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.178 + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.179
1.180
1.181 "----- d2_pqformula10_neg ------";
1.182 @@ -467,7 +467,7 @@
1.183 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.184 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.185 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.186 - | _ => raise error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
1.187 + | _ => error "polyeq.sml: diff.behav. in -4 + 1*x^2 = 0 -> [x = 2, x = -2]";
1.188
1.189 "----- d2_pqformula9_neg ------";
1.190 val fmz = ["equality (4 + 1*x^^^2 = 0)", "solveFor x","solutions L"];
1.191 @@ -508,7 +508,7 @@
1.192 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.193 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.194 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -1 / 2]")) => ()
1.195 - | _ => raise error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
1.196 + | _ => error "polyeq.sml: diff.behav. in -1 + (-1)*x + 2*x^2 = 0 -> [x = 1, x = -1/2]";
1.197
1.198 val fmz = ["equality ( 1 +(-1)*x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.199 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.200 @@ -545,7 +545,7 @@
1.201 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.202 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.203 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 2, x = -1]")) => ()
1.204 - | _ => raise error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
1.205 + | _ => error "polyeq.sml: diff.behav. in -1 + x + 2*x^2 = 0 -> [x = 1/2, x = -1]";
1.206
1.207 val fmz = ["equality ( 1 + x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.208 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.209 @@ -582,7 +582,7 @@
1.210 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.211 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.212 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
1.213 - | _ => raise error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
1.214 + | _ => error "polyeq.sml: diff.behav. in -2 + 1*x + x^2 = 0 -> [x = 1, x = -2]";
1.215
1.216 val fmz = ["equality ( 2 + 1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.217 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.218 @@ -620,7 +620,7 @@
1.219 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.220 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.221 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1, x = -2]")) => ()
1.222 - | _ => raise error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
1.223 + | _ => error "polyeq.sml: diff.behav. in -2 + x + x^2 = 0 -> [x = 1, x = -2]";
1.224
1.225 val fmz = ["equality ( 2 + x + x^^^2 = 0)", "solveFor x","solutions L"];
1.226 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.227 @@ -658,7 +658,7 @@
1.228 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.229 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.230 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.231 - | _ => raise error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
1.232 + | _ => error "polyeq.sml: diff.behav. in -8 + 2*x^2 = 0 -> [x = 2, x = -2]";
1.233
1.234 val fmz = ["equality ( 8+ 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.235 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.236 @@ -694,7 +694,7 @@
1.237 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.238 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.239 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.240 - | _ => raise error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.241 + | _ => error "polyeq.sml: diff.behav. in -4 + x^2 = 0 -> [x = 2, x = -2]";
1.242
1.243
1.244 val fmz = ["equality ( 4+ x^^^2 = 0)", "solveFor x","solutions L"];
1.245 @@ -731,7 +731,7 @@
1.246 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.247 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.248 case f of Form' (FormKF (~1,EdUndef,_,Nundef,"[x = 0, x = -1]")) => ()
1.249 - | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.250 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.251
1.252 val fmz = ["equality (1*x + x^^^2 = 0)", "solveFor x","solutions L"];
1.253 val (dI',pI',mI') = ("PolyEq",["abcFormula","degree_2","polynomial","univariate","equation"],
1.254 @@ -749,7 +749,7 @@
1.255 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.256 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.257 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.258 - | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.259 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.260
1.261 (*EP-16*)
1.262 val fmz = ["equality (x + 2*x^^^2 = 0)", "solveFor x","solutions L"];
1.263 @@ -768,7 +768,7 @@
1.264 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.265 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.266 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1 / 2]")) => ()
1.267 - | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
1.268 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1 / 2]";
1.269
1.270 (*EP-//*)
1.271 val fmz = ["equality (x + x^^^2 = 0)", "solveFor x","solutions L"];
1.272 @@ -787,7 +787,7 @@
1.273 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.274 val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.275 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = -1]")) => ()
1.276 - | _ => raise error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.277 + | _ => error "polyeq.sml: diff.behav. in x + x^2 = 0 -> [x = 0, x = -1]";
1.278
1.279 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.280 "----------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b----";
1.281 @@ -835,10 +835,10 @@
1.282 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.283 (* FIXXXME
1.284 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => () TODO
1.285 - | _ => raise error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
1.286 + | _ => error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
1.287 *)
1.288 if f2str f = "[x = -1 * -1 + -1 * sqrt (1 ^^^ 2 - -8),\n x = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))]" then ()
1.289 -else raise error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
1.290 +else error "polyeq.sml corrected?behav. in [x = -2, x = 4]";
1.291
1.292
1.293 "-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
1.294 @@ -849,7 +849,7 @@
1.295 val SOME (t,_) = rewrite_set_ PolyEq.thy false PolyEq_erls t1;
1.296 val t' = term2str t;
1.297 (*if t'= "True" then ()
1.298 - else raise error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1.299 + else error "polyeq.sml: diff.behav. in 'rewrite_set_.. PolyEq_erls";*)
1.300 (* *)
1.301 val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
1.302 "solveFor x","solutions L"];
1.303 @@ -904,7 +904,7 @@
1.304 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.305 (* FIXXXXME n1.,
1.306 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => () TODO
1.307 - | _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
1.308 + | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
1.309 *)
1.310
1.311 "----------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2,S.68Nr.44.a*)";
1.312 @@ -946,7 +946,7 @@
1.313 (~1,EdUndef,0,Nundef,
1.314 "[x = (a + b) / 2 + -1 * sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b)]"))
1.315 => ()
1.316 - | _ => raise error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
1.317 + | _ => error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
1.318 this will be simplified [x = a, x = b] to by Factor.ML*)
1.319
1.320
1.321 @@ -978,7 +978,7 @@
1.322 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.323 (*WN.2.5.03 TODO "[x = sqrt (0 - -64), x = -1 * sqrt (0 - -64)]"
1.324 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
1.325 - | _ => raise error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
1.326 + | _ => error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
1.327 *)
1.328
1.329 "----------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b------*)";
1.330 @@ -1004,10 +1004,10 @@
1.331 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.332 (*WN.2.5.03 TODO "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]"
1.333 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
1.334 - | _ => raise error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
1.335 + | _ => error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
1.336 *)
1.337 if f2str f = "[x = sqrt (0 - -49), x = -1 * sqrt (0 - -49)]" then ()
1.338 -else raise error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
1.339 +else error "polyeq.sml CORRECTED?behav. in [x = 7, x = -7]";
1.340
1.341
1.342 "----------- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk Is86Bsp5";
1.343 @@ -1052,7 +1052,7 @@
1.344 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.345 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.346 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
1.347 - | _ => raise error "polyeq.sml: diff.behav. in [x = 2]";
1.348 + | _ => error "polyeq.sml: diff.behav. in [x = 2]";
1.349
1.350
1.351 "----------- ((x+1)*(x+2) - (3*x - 2)^^^2=.. Schalk II s.68 Bsp 37";
1.352 @@ -1097,7 +1097,7 @@
1.353 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.354 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.355 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
1.356 - | _ => raise error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
1.357 + | _ => error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
1.358
1.359
1.360 " -4 + x^^^2 =0 ";
1.361 @@ -1121,7 +1121,7 @@
1.362 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.363 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.364 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
1.365 - | _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
1.366 + | _ => error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
1.367
1.368 "----------------- polyeq.sml end ------------------";
1.369