1.1 --- a/test/Tools/isac/Knowledge/rational.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -68,120 +68,120 @@
1.4 print("\n\n***** divide tests *****\n");
1.5 val mv_pquot1 = (#1(mv_division([(1,[1,1,1]),(1,[1,1,0]),(1,[1,0,1]),(1,[0,0,0])],[(1,[1,1,0]),(1,[0,0,0])],LEX_)));
1.6 (* result: [(1,[0,0,1]),(1,[0,0,0])] *)
1.7 -if mv_pquot1=[(1,[0,0,1]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.8 +if mv_pquot1=[(1,[0,0,1]),(1,[0,0,0])] then () else error ("rational.sml: example failed");
1.9
1.10 val mv_prest1 = (#2(mv_division([(1,[1,1,1]),(1,[1,1,0]),(1,[1,0,1]),(1,[0,0,0])],[(1,[1,1,0]),(1,[0,0,0])],LEX_)));
1.11 (* result: [(1,[1,0,1]),(~1,[0,0,1])] *)
1.12 -if mv_prest1=[(1,[1,0,1]),(~1,[0,0,1])] then () else raise error ("rational.sml: example failed");
1.13 +if mv_prest1=[(1,[1,0,1]),(~1,[0,0,1])] then () else error ("rational.sml: example failed");
1.14
1.15 val mv_pquot2 = (#1(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
1.16 (* result: [(4,[1]),(4,[0])] *)
1.17 -if mv_pquot2=[(4,[1]),(4,[0])] then () else raise error ("rational.sml: example failed");
1.18 +if mv_pquot2=[(4,[1]),(4,[0])] then () else error ("rational.sml: example failed");
1.19
1.20 val mv_prest2 = (#2(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
1.21 (* result: [(12,[0]] *)
1.22 -if mv_prest2=[(12,[0])] then () else raise error ("rational.sml: example failed");
1.23 +if mv_prest2=[(12,[0])] then () else error ("rational.sml: example failed");
1.24
1.25 val mv_pquot3 = (#1(mv_division([(4,[2]),(~4,[0])],[(2,[1]),(2,[0])],LEX_)));
1.26 (* [(2,[1]),(~2,[0])] *)
1.27 -if mv_pquot3=[(2,[1]),(~2,[0])] then () else raise error ("rational.sml: example failed");
1.28 +if mv_pquot3=[(2,[1]),(~2,[0])] then () else error ("rational.sml: example failed");
1.29
1.30 val mv_prest3 = (#2(mv_division([(1,[2]),(~1,[0])],[(2,[1]),(2,[0])],LEX_)));
1.31 (* [(1,[2]),(~1,[0])] *)
1.32 -if mv_prest3=[(1,[2]),(~1,[0])] then () else raise error ("rational.sml: example failed");
1.33 +if mv_prest3=[(1,[2]),(~1,[0])] then () else error ("rational.sml: example failed");
1.34
1.35 val mv_pquot4 = (#1(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1])],[(2,[1,0,0]),(4,[0,0,1])],LEX_)));
1.36 (* [(1,[0,1,1])] *)
1.37 -if mv_pquot4=[(1,[0,1,1])] then () else raise error ("rational.sml: example failed");
1.38 +if mv_pquot4=[(1,[0,1,1])] then () else error ("rational.sml: example failed");
1.39
1.40 val mv_prest4 = (#2(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1])],[(2,[1,0,0]),(4,[0,0,1])],GGO_)));
1.41 (* [(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] *)
1.42 -if mv_prest4 =[(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
1.43 +if mv_prest4 =[(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] then () else error ("rational.sml: example failed");
1.44
1.45 val mv_pquot5 = (#1(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1]),(6,[2,1,3]),(4,[0,4,1]),(1,[2,2,1])],[(1,[0,0,1])],LEX_)));
1.46 (* [(1,[2,2,0]),(6,[2,1,2]),(3,[1,1,0]),(4,[1,0,0]),(4,[0,4,0]),(3,[0,0,0])]*)
1.47 -if mv_pquot5=[(1,[2,2,0]),(6,[2,1,2]),(3,[1,1,0]),(4,[1,0,0]),(4,[0,4,0]),(3,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.48 +if mv_pquot5=[(1,[2,2,0]),(6,[2,1,2]),(3,[1,1,0]),(4,[1,0,0]),(4,[0,4,0]),(3,[0,0,0])] then () else error ("rational.sml: example failed");
1.49
1.50 val mv_prest5 = (#2(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1]),(6,[2,1,3]),(4,[0,4,1]),(1,[2,2,1])],[(1,[0,0,1])],LEX_)));
1.51 (* [] *)
1.52 -if mv_prest5=[] then () else raise error ("rational.sml: example failed");
1.53 +if mv_prest5=[] then () else error ("rational.sml: example failed");
1.54
1.55 (* (x^2 + 2(a+1)x + (a^2+2a+1)) / (x+a+1) = x+a+1 *)
1.56 val mv_pquot6 = (#1(mv_division([(1,[2,0,0]),(2,[1,1,0]),(2,[1,0,0]),(1,[0,2,0]),(2,[0,1,0]),(1,[0,0,0])],[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])],LEX_)));
1.57 -if mv_pquot6=[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.58 +if mv_pquot6=[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])] then () else error ("rational.sml: example failed");
1.59
1.60 val mv_prest6 = (#2(mv_division([(1,[2,0,0]),(2,[1,1,0]),(2,[1,0,0]),(1,[0,2,0]),(2,[0,1,0]),(1,[0,0,0])],[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])],LEX_)));
1.61 -if mv_prest6=[] then () else raise error ("rational.sml: example failed");
1.62 +if mv_prest6=[] then () else error ("rational.sml: example failed");
1.63
1.64
1.65 print("\n\n***** MV_CONTENT-TESTS *****\n");
1.66 val mv_cont1=mv_content([(1,[2,1]),(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
1.67 (* [(1,[0,1]),(1,[0,0])] *)
1.68 -if mv_cont1=[(1,[0,1]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
1.69 +if mv_cont1=[(1,[0,1]),(1,[0,0])] then () else error ("rational.sml: example failed");
1.70
1.71 val mv_pp1=mv_pp([(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
1.72 (*[(1,[1,0]),(1,[0,0])]*)
1.73 -if mv_pp1=[(1,[1,0]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
1.74 +if mv_pp1=[(1,[1,0]),(1,[0,0])] then () else error ("rational.sml: example failed");
1.75
1.76 val mv_cont2=mv_content([(2,[1]),(4,[0])]);
1.77 (* [(2,[0])] *)
1.78 -if mv_cont2=[(2,[0])] then () else raise error ("rational.sml: example failed");
1.79 +if mv_cont2=[(2,[0])] then () else error ("rational.sml: example failed");
1.80
1.81 val mv_pp2=mv_pp([(2,[1]),(4,[0])]);
1.82 (* [(1,[1]),(2,[0])] *)
1.83 -if mv_pp2=[(1,[1]),(2,[0])] then () else raise error ("rational.sml: example failed");
1.84 +if mv_pp2=[(1,[1]),(2,[0])] then () else error ("rational.sml: example failed");
1.85
1.86 val mv_cont3=mv_content[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
1.87 (* [(2,[0,0,0])] *)
1.88 -if mv_cont3=[(2,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.89 +if mv_cont3=[(2,[0,0,0])] then () else error ("rational.sml: example failed");
1.90
1.91 val mv_pp3=mv_pp[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
1.92 (* [(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] *)
1.93 -if mv_pp3=[(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] then () else raise error ("rational.sml: example failed");
1.94 +if mv_pp3=[(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] then () else error ("rational.sml: example failed");
1.95
1.96 val mv_cont4=mv_content[(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
1.97 (* [(1,[0,0,0])] *)
1.98 -if mv_cont4=[(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.99 +if mv_cont4=[(1,[0,0,0])] then () else error ("rational.sml: example failed");
1.100
1.101 val mv_pp4=mv_pp [(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
1.102 (* [(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] *)
1.103 -if mv_pp4=[(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
1.104 +if mv_pp4=[(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] then () else error ("rational.sml: example failed");
1.105
1.106 val con1=mv_content([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
1.107 (* [(3,[0,0])] *)
1.108 -if con1=[(3,[0,0])] then () else raise error ("rational.sml: example failed");
1.109 +if con1=[(3,[0,0])] then () else error ("rational.sml: example failed");
1.110
1.111 val pp1=mv_pp([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
1.112 (* [(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] *)
1.113 -if pp1=[(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] then () else raise error ("rational.sml: example failed");
1.114 +if pp1=[(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] then () else error ("rational.sml: example failed");
1.115
1.116 val con2=mv_content([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
1.117 (* [(1,[0,0])] *)
1.118 -if con2=[(1,[0,0])] then () else raise error ("rational.sml: example failed");
1.119 +if con2=[(1,[0,0])] then () else error ("rational.sml: example failed");
1.120
1.121 val pp2 =mv_pp([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
1.122 (* [(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] *)
1.123 -if pp2=[(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] then () else raise error ("rational.sml: example failed");
1.124 +if pp2=[(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] then () else error ("rational.sml: example failed");
1.125
1.126 val cont1 = mv_content [(1,[2,1,0]),(2,[2,1,0])];
1.127 (* [(3,[0,1,0])] *)
1.128 -if cont1=[(3,[0,1,0])] then () else raise error ("rational.sml: example failed");
1.129 +if cont1=[(3,[0,1,0])] then () else error ("rational.sml: example failed");
1.130
1.131 val pp1 = mv_pp [(1,[2,1,0]),(2,[2,1,0])];
1.132 (* [(1,[2,0,0])] *)
1.133 -if pp1=[(1,[2,0,0])] then () else raise error ("rational.sml: example failed");
1.134 +if pp1=[(1,[2,0,0])] then () else error ("rational.sml: example failed");
1.135
1.136 val cont2 = mv_content [(4,[1,2,0]),(2,[2,1,0])];
1.137 (* [(2,[0,1,0])] *)
1.138 -if cont2=[(2,[0,1,0])] then () else raise error ("rational.sml: example failed");
1.139 +if cont2=[(2,[0,1,0])] then () else error ("rational.sml: example failed");
1.140
1.141 val pp2 = mv_pp [(4,[1,2,0]),(2,[2,1,0])];
1.142 (* [(1,[2,0,0]),(2,[1,1,0])] *)
1.143 -if pp2=[(1,[2,0,0]),(2,[1,1,0])] then () else raise error ("rational.sml: example failed");
1.144 +if pp2=[(1,[2,0,0]),(2,[1,1,0])] then () else error ("rational.sml: example failed");
1.145
1.146 print("\n\n\n\n********************************************************\n\n");
1.147 val cont3=mv_content [(65,[3,2,2]),(52,[3,2,1]),(26,[3,1,2]),(~95,[2,2,3]),(~76,[2,2,2]),(35,[2,2,1]),(28,[2,2,0]),(~38,[2,1,3]),(14,[2,1,1])];
1.148 -if cont3=[(5,[0,2,1]),(4,[0,2,0]),(2,[0,1,1])] then () else raise error ("rational.sml: example failed");
1.149 +if cont3=[(5,[0,2,1]),(4,[0,2,0]),(2,[0,1,1])] then () else error ("rational.sml: example failed");
1.150 val pp3=mv_pp [(65,[3,2,2]),(52,[3,2,1]),(26,[3,1,2]),(~95,[2,2,3]),(~76,[2,2,2]),(35,[2,2,1]),(28,[2,2,0]),(~38,[2,1,3]),(14,[2,1,1])];
1.151
1.152
1.153 @@ -213,60 +213,60 @@
1.154 print("\n\n***** mv_gcd-tests *****\n");
1.155 val ggt1 = mv_gcd [(4,[2,2]),(8,[1,1]),(4,[0,0])] [(2,[1,1]),(2,[0,0])];
1.156 (* [(2,[1,1]),(2,[0,0])] *)
1.157 -if ggt1=[(2,[1,1]),(2,[0,0])] then () else raise error ("rational.sml: example failed");
1.158 +if ggt1=[(2,[1,1]),(2,[0,0])] then () else error ("rational.sml: example failed");
1.159
1.160 val ggt2 = mv_gcd [(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(15,[1,1,1])] [(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
1.161 (* [(2,[1,1,0]),(3,[0,0,1])] *)
1.162 -if ggt2=[(2,[1,1,0]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
1.163 +if ggt2=[(2,[1,1,0]),(3,[0,0,1])] then () else error ("rational.sml: example failed");
1.164
1.165
1.166 val ggt3 = mv_gcd [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
1.167 (* [(1,[1,0]),(~1,[0,1])] *)
1.168 -if ggt3=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
1.169 +if ggt3=[(1,[1,0]),(~1,[0,1])] then () else error ("rational.sml: example failed");
1.170
1.171
1.172 val ggt4 = mv_gcd [(1,[2,1,0]),(2,[2,1,0])] [(5,[1,0,0])];
1.173 (* [(1,[1,0,0])] *)
1.174 -if ggt4=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
1.175 +if ggt4=[(1,[1,0,0])] then () else error ("rational.sml: example failed");
1.176
1.177
1.178 val ggt5 = mv_gcd [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
1.179 (* [(1,[1,0]),(~1,[0,1])] *)
1.180 -if ggt5=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
1.181 +if ggt5=[(1,[1,0]),(~1,[0,1])] then () else error ("rational.sml: example failed");
1.182
1.183
1.184 val ggt6 = mv_gcd [(10,[2,1,1]),(14,[1,1,0]),(3,[1,0,1]),(20,[1,2,1])] [(5,[1,1,1]),(7,[2,1,1])];
1.185 (* [(1,[0,0,0])] *)
1.186 -if ggt6=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
1.187 +if ggt6=[(1,[1,0,0])] then () else error ("rational.sml: example failed");
1.188
1.189 print("\n\n***** kgv-tests *****\n");
1.190 val kgv1=mv_lcm [(10,[])] [(15,[])];
1.191 (* [(30,[])] *)
1.192 -if kgv1=[(30,[])] then () else raise error ("rational.sml: example failed");
1.193 +if kgv1=[(30,[])] then () else error ("rational.sml: example failed");
1.194
1.195 val kgv2=mv_lcm [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
1.196 (* [(1,[2,0]),(~2,[1,1]),(1,[0,2])] *)
1.197 -if kgv2=[(1,[2,0]),(~2,[1,1]),(1,[0,2])] then () else raise error ("rational.sml: example failed");
1.198 +if kgv2=[(1,[2,0]),(~2,[1,1]),(1,[0,2])] then () else error ("rational.sml: example failed");
1.199
1.200 val kgv3=mv_lcm [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
1.201 (* [(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] *)
1.202 -if kgv3=[(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] then () else raise error ("rational.sml: example failed");
1.203 +if kgv3=[(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] then () else error ("rational.sml: example failed");
1.204
1.205 (*!!!--------
1.206 print("\n\n***** STEP_CANCEL_TESTS: *****\n");
1.207
1.208 val term2 = (term_of o the o (parse thy)) " (9 * a^^^2 * b) / (6 * a * c)";
1.209 val div2 = term2str (step_cancel term2);
1.210 -if div2 = "3 * (a * b) * (3 * a) / (2 * c * (3 * a))" then () else raise error ("rational.sml: example failed");
1.211 +if div2 = "3 * (a * b) * (3 * a) / (2 * c * (3 * a))" then () else error ("rational.sml: example failed");
1.212
1.213
1.214 val term1 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) / a";
1.215 val div1 = term2str(step_cancel term1);
1.216 -if div1 = "(3 * c + 14 * b + 20 * (b ^^^ 2 * c) + 10 * (a * (b * c))) * a / (1 * a)" then () else raise error ("rational.sml: example failed");
1.217 +if div1 = "(3 * c + 14 * b + 20 * (b ^^^ 2 * c) + 10 * (a * (b * c))) * a / (1 * a)" then () else error ("rational.sml: example failed");
1.218
1.219 val term3 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c) / (1 * x * y * z) ";
1.220 val div3 = term2str(step_cancel term3);
1.221 -if div3="10 * a ^^^ 2 * b * c / (1 * x * y * z)" then () else raise error ("rational.sml: example failed");
1.222 +if div3="10 * a ^^^ 2 * b * c / (1 * x * y * z)" then () else error ("rational.sml: example failed");
1.223
1.224 --------------------------------------------------------------------------!!!*)
1.225
1.226 @@ -430,16 +430,16 @@
1.227 val SOME (t'',_) = add_fraction_ thy t;
1.228 if term2str t' = "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x))\
1.229 \ +\n1 * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" then ()
1.230 -else raise error "rational.sml lex-ord 1";
1.231 +else error "rational.sml lex-ord 1";
1.232 if term2str t'' = "(-1 - y - x) / (y - x)" then ()
1.233 -else raise error "rational.sml lex-ord 2";
1.234 +else error "rational.sml lex-ord 2";
1.235 (*WN.16.10.02 WN070905 lexicographische Ordnung erhalten ! SK.ord*)
1.236
1.237
1.238 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)";
1.239 val SOME (t',_) = norm_expanded_rat_ thy t;
1.240 if term2str t' = "(x + y) / (x - y)" then ()
1.241 -else raise error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 1";
1.242 +else error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 1";
1.243 (*val SOME (t'',_) = norm_rational_ thy t;
1.244 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
1.245 WN.16.10.02 ?! + WN060831???SK4
1.246 @@ -449,7 +449,7 @@
1.247 val t = str2term "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
1.248 val SOME (t',_) = norm_expanded_rat_ thy t;
1.249 if term2str t' = "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)" then ()
1.250 -else raise error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +...";
1.251 +else error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +...";
1.252 (*val SOME (t'',_) = norm_rational_ thy t;
1.253 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?!
1.254 WN070906 *** term2poly: invalid = 9 - x ^^^ 2 SK.term2poly*)
1.255 @@ -510,7 +510,7 @@
1.256 is_expanded (parse_rat "8 * x + -8");
1.257 (* e188a = ("8 / 9",["not ((-1) + x = 0)"]) then () 13.3.03*)
1.258 if e188a = ("8 / 9",["-1 + x ~= 0"]) then ()
1.259 -else raise error "rational.sml: e188a new behaviour";
1.260 +else error "rational.sml: e188a new behaviour";
1.261 val SOME (t,_) = rewrite_set thy' false mp
1.262 "(8*((-1) + x))/(9*((-1) + x))";
1.263 print("b)\n");
1.264 @@ -525,7 +525,7 @@
1.265 val SOME (t,_) =
1.266 rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
1.267 if t= "(a + -1 * b) / (-1 * a + b)" then()
1.268 -else raise error "rational.sml: e188c new behaviour";
1.269 +else error "rational.sml: e188c new behaviour";
1.270
1.271 print("\n\nexample 190:\n");
1.272 print("c)\n");
1.273 @@ -533,7 +533,7 @@
1.274 val e190c = the (rewrite_set thy' false "cancel" e190c');
1.275 val SOME (t,_) = rewrite_set thy' false mp "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
1.276 if t = "(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)" then ()
1.277 -else raise error "rational.sml: e190c new behaviour";
1.278 +else error "rational.sml: e190c new behaviour";
1.279
1.280 print("\n\nexample 191:\n");
1.281 print("a)\n");
1.282 @@ -547,7 +547,7 @@
1.283 val SOME (t,_) = rewrite_set thy' false mp "((x + (-1) * y)*(x + y))/((1)*(x + y))";
1.284 (* t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() WN.13.3.03*)
1.285 if t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then()
1.286 -else raise error "rational.sml: e191a new behaviour";
1.287 +else error "rational.sml: e191a new behaviour";
1.288
1.289 print("c)\n");
1.290 val e191c'="( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )";
1.291 @@ -562,7 +562,7 @@
1.292 val SOME (t,_) = rewrite_set thy' false mp "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
1.293 (* t="(25 + ((-30) * x + 9 * x ^^^ 2)) / ((-25) + 9 * x ^^^ 2)"then() 13.3.03*)
1.294 if t= "(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)" then()
1.295 -else raise error "rational.sml: 'e191c' new behaviour";
1.296 +else error "rational.sml: 'e191c' new behaviour";
1.297
1.298
1.299 print("\n\nexample 192:\n");
1.300 @@ -574,11 +574,11 @@
1.301 val SOME (t',_) = rewrite_set thy' false mp "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1.302 if t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)"
1.303 (*"(-1 * y * x ^^^ 2 + 7 * x ^^^ 3) / (-1 * y ^^^ 3 + 7 * x * y ^^^ 2)"WN050929*)
1.304 -then () else raise error "rational.sml: 'e192b' new behaviour";
1.305 +then () else error "rational.sml: 'e192b' new behaviour";
1.306 (*^^^ works with MG's simplifier vvv*)
1.307 val t =str2term"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1.308 val SOME (t',_) = rewrite_set_ Isac.thy false make_polynomial t;
1.309 -if term2str t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)" then () else raise error "rational.sml: 'e192b'MG new behaviour";
1.310 +if term2str t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)" then () else error "rational.sml: 'e192b'MG new behaviour";
1.311
1.312
1.313 print("\n\nexample 193:\n");
1.314 @@ -600,7 +600,7 @@
1.315 val SOME (t,_) = rewrite_set thy' false "cancel" wn01;
1.316 (* t = "((-5) + 3 * x) / 1" then () WN.13.3.03*)
1.317 if t = "(-5 + 3 * x) / 1" then ()
1.318 -else raise error "rational.sml: new behav. in cancel wn01";
1.319 +else error "rational.sml: new behav. in cancel wn01";
1.320
1.321
1.322 "-------- common_nominator_p ---------------------------- --------";
1.323 @@ -838,7 +838,7 @@
1.324 val est1'="(7) / (-14) + (-2) / (4)";
1.325 val est1 = the (rewrite_set thy' false "common_nominator_p" est1');
1.326 if est1 = ("-1 / 1",[]) then ()
1.327 -else raise error "new behaviour in rational.sml: est1'";
1.328 +else error "new behaviour in rational.sml: est1'";
1.329
1.330 val t = (term_of o the o (parse thy))
1.331 "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
1.332 @@ -909,7 +909,7 @@
1.333 val (r,(t,asm))::_ = loc revsets t r;
1.334 val ss = term2str t;
1.335 if ss = "(3 - x) / (3 + x)" then ()
1.336 - else raise error "rational.sml: new behav. in rev-set cancel";
1.337 + else error "rational.sml: new behav. in rev-set cancel";
1.338 terms2str asm;
1.339
1.340
1.341 @@ -963,18 +963,18 @@
1.342 "-------- norm_Rational ------------------------------------------";
1.343 val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
1.344 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.345 -if term2str t' = "1 / 18 = 0" then () else raise error "rational.sml 1";
1.346 +if term2str t' = "1 / 18 = 0" then () else error "rational.sml 1";
1.347
1.348 val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
1.349 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.350 if term2str t' = "(237 + 65 * x) / 36 = 0" then ()
1.351 -else raise error "rational.sml 2";
1.352 +else error "rational.sml 2";
1.353
1.354 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
1.355 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.356 (*before 040209:if term2str t' = "(23 + (35 * x + -72 * x ^^^ 2)) / 1"then()*)
1.357 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
1.358 -else raise error "rational.sml 3";
1.359 +else error "rational.sml 3";
1.360 (*trace_rewrite:=true;*)
1.361 val t = str2term "Not (6*x is_atom)";
1.362 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
1.363 @@ -990,37 +990,37 @@
1.364
1.365 val t = str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";
1.366 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.367 -if term2str t' = "65 * x / 2" then () else raise error "rational.sml 4";
1.368 +if term2str t' = "65 * x / 2" then () else error "rational.sml 4";
1.369
1.370 val t = str2term "1 - ((13*x)/2 - 5/2)^^^2";
1.371 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.372 (*bef.040209: if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4"then()*)
1.373 if term2str t' = "(-21 + 130 * x + -169 * x ^^^ 2) / 4" then ()
1.374 -else raise error "rational.sml 5";
1.375 +else error "rational.sml 5";
1.376
1.377 (*SRAM Schalk I, p.92 Nr. 609a*)
1.378 val t = str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";
1.379 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.380 if term2str t' = "(-255 + 112 * x) / 135" then ()
1.381 -else raise error "rational.sml 6";
1.382 +else error "rational.sml 6";
1.383
1.384 (*SRAM Schalk I, p.92 Nr. 610c*)
1.385 val t = str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2";
1.386 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.387 -if term2str t' = "(-3 + -1 * x) / 2" then () else raise error "rational.sml 7";
1.388 +if term2str t' = "(-3 + -1 * x) / 2" then () else error "rational.sml 7";
1.389
1.390 (*SRAM Schalk I, p.92 Nr. 476a*)
1.391 val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) *\
1.392 \ (1 + x)";(*. a/b : c/d translated to a/b * d/c .*)
1.393 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.394 -(*if term2str t' = "1 / 1" then () else raise error "rational.sml 8";3.6.03*)
1.395 -if term2str t' = "1" then () else raise error "rational.sml 8";
1.396 +(*if term2str t' = "1 / 1" then () else error "rational.sml 8";3.6.03*)
1.397 +if term2str t' = "1" then () else error "rational.sml 8";
1.398
1.399 (*............................vvv---TODO: sollte gehen mit poly_order *)
1.400 (*Schalk I, p.92 Nr. 472a*)
1.401 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";
1.402 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.403 -if term2str t' = "x + y" then () else raise error "rational.sml p.92 Nr. 472a";
1.404 +if term2str t' = "x + y" then () else error "rational.sml p.92 Nr. 472a";
1.405
1.406 (*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
1.407 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1.408 @@ -1067,14 +1067,14 @@
1.409 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.410 term2str t;
1.411 if (term2str t) = "19 / 21" then ()
1.412 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 1";
1.413 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 1";
1.414
1.415 (*SRA Schalk I, p.40 Nr. 166a *)
1.416 val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
1.417 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.418 term2str t;
1.419 if (term2str t) = "45 / 2" then ()
1.420 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 2";
1.421 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 2";
1.422
1.423
1.424 "-------- cancellation -------------------------------------------";
1.425 @@ -1089,7 +1089,7 @@
1.426 if (term2str t) =
1.427 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.428 then ()
1.429 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 3";
1.430 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 3";
1.431
1.432 (* e192b Stefan K.*)
1.433 val t = str2term
1.434 @@ -1099,7 +1099,7 @@
1.435 if (term2str t) =
1.436 "x ^^^ 2 / y ^^^ 2"
1.437 then ()
1.438 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 4";
1.439 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 4";
1.440
1.441 (*SRC Schalk I, p.66 Nr. 379c *)
1.442 val t = str2term
1.443 @@ -1109,7 +1109,7 @@
1.444 if (term2str t) =
1.445 "-1"
1.446 then ()
1.447 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 5";
1.448 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 5";
1.449
1.450 (*SRC Schalk I, p.66 Nr. 380b *)
1.451 val t = str2term
1.452 @@ -1119,7 +1119,7 @@
1.453 if (term2str t) =
1.454 "(27 + 12 * x) / (28 + 8 * x)"
1.455 then ()
1.456 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 6";
1.457 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 6";
1.458
1.459 (*Schalk I, p.60 Nr. 215c *)
1.460 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*)
1.461 @@ -1130,7 +1130,7 @@
1.462 if (term2str t) =
1.463 "(a ^^^ 4 * x + -1 * a ^^^ 4 * y + 4 * a ^^^ 3 * b * x + -4 * a ^^^ 3 * b * y + 6 * a ^^^ 2 * b ^^^ 2 * x + -6 * a ^^^ 2 * b ^^^ 2 * y + 4 * a * b ^^^ 3 * x + -4 * a * b ^^^ 3 * y + b ^^^ 4 * x + -1 * b ^^^ 4 * y) /(a ^^^ 2 * x ^^^ 3 + -3 * a ^^^ 2 * x ^^^ 2 * y + 3 * a ^^^ 2 * x * y ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 3 + 2 * a * b * x ^^^ 3 + -6 * a * b * x ^^^ 2 * y + 6 * a * b * x * y ^^^ 2 + -2 * a * b * y ^^^ 3 + b ^^^ 2 * x ^^^ 3 + -3 * b ^^^ 2 * x ^^^ 2 * y + 3 * b ^^^ 2 * x * y ^^^ 2 + -1 * b ^^^ 2 * y ^^^ 3)"
1.464 then ()
1.465 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 7";
1.466 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 7";
1.467 *)
1.468 (*val t = str2term
1.469 "(a ^^^ 4 * x + -1 * a ^^^ 4 * y + 4 * a ^^^ 3 * b * x + -4 * a ^^^ 3 * b * y + 6 * a ^^^ 2 * b ^^^ 2 * x + -6 * a ^^^ 2 * b ^^^ 2 * y + 4 * a * b ^^^ 3 * x + -4 * a * b ^^^ 3 * y + b ^^^ 4 * x + -1 * b ^^^ 4 * y) /(a ^^^ 2 * x ^^^ 3 + -3 * a ^^^ 2 * x ^^^ 2 * y + 3 * a ^^^ 2 * x * y ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 3 + 2 * a * b * x ^^^ 3 + -6 * a * b * x ^^^ 2 * y + 6 * a * b * x * y ^^^ 2 + -2 * a * b * y ^^^ 3 + b ^^^ 2 * x ^^^ 3 + -3 * b ^^^ 2 * x ^^^ 2 * y + 3 * b ^^^ 2 * x * y ^^^ 2 + -1 * b ^^^ 2 * y ^^^ 3)"
1.470 @@ -1147,7 +1147,7 @@
1.471 term2str t;
1.472 if (term2str t) =
1.473 "(a + b) / (4 * a + -4 * b)"
1.474 -then () else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
1.475 +then () else error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
1.476 *)
1.477
1.478 (*SRC Schalk I, p.66 Nr. 381b *)
1.479 @@ -1158,7 +1158,7 @@
1.480 if (term2str t) =
1.481 "-1 / (5 + -2 * x)"
1.482 then ()
1.483 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 9";
1.484 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 9";
1.485
1.486 (*SRC Schalk I, p.66 Nr. 381c *)
1.487 val t = str2term
1.488 @@ -1168,7 +1168,7 @@
1.489 if (term2str t) =
1.490 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.491 then ()
1.492 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 10";
1.493 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 10";
1.494
1.495 (*SRC Schalk I, p.66 Nr. 383a *)
1.496 val t = str2term
1.497 @@ -1178,7 +1178,7 @@
1.498 if (term2str t) =
1.499 "5 * a / (a + -1 * b)"
1.500 then ()
1.501 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 11";
1.502 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 11";
1.503
1.504 "-------- common denominator -------------------------------------";
1.505 "-------- common denominator -------------------------------------";
1.506 @@ -1192,7 +1192,7 @@
1.507 if (term2str t) =
1.508 "(-3 * x + 4 * y + -1 * x * y) / (x * y)"
1.509 then ()
1.510 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 12";
1.511 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 12";
1.512
1.513 (*SRA Schalk I, p.67 Nr. 407b *)
1.514 val t = str2term
1.515 @@ -1202,7 +1202,7 @@
1.516 if (term2str t) =
1.517 "4 / c"
1.518 then ()
1.519 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 13";
1.520 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 13";
1.521
1.522 (*SRA Schalk I, p.67 Nr. 410b *)
1.523 val t = str2term
1.524 @@ -1212,7 +1212,7 @@
1.525 if (term2str t) =
1.526 "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
1.527 then ()
1.528 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 14";
1.529 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 14";
1.530
1.531 (*SRA Schalk I, p.67 Nr. 413b *)
1.532 val t = str2term
1.533 @@ -1222,7 +1222,7 @@
1.534 if (term2str t) =
1.535 "6 * x / (1 + -1 * x ^^^ 2)"
1.536 then ()
1.537 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 15";
1.538 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 15";
1.539
1.540 (*SRA Schalk I, p.68 Nr. 414a *)
1.541 val t = str2term
1.542 @@ -1232,7 +1232,7 @@
1.543 if (term2str t) =
1.544 "(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
1.545 then ()
1.546 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 16";
1.547 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 16";
1.548
1.549 (*SRA Schalk I, p.68 Nr. 423a *)
1.550 val t = str2term
1.551 @@ -1242,7 +1242,7 @@
1.552 if (term2str t) =
1.553 "1"
1.554 then ()
1.555 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 17";
1.556 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 17";
1.557
1.558 (*SRA Schalk I, p.68 Nr. 428b *)
1.559 val t = str2term
1.560 @@ -1252,7 +1252,7 @@
1.561 if (term2str t) =
1.562 "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
1.563 then ()
1.564 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 18";
1.565 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 18";
1.566
1.567 (*SRA Schalk I, p.68 Nr. 430b *)
1.568 val t = str2term
1.569 @@ -1262,7 +1262,7 @@
1.570 if (term2str t) =
1.571 "a + 3 * b"
1.572 then ()
1.573 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 19";
1.574 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 19";
1.575
1.576
1.577 (*SRA Schalk I, p.68 Nr. 432 *)
1.578 @@ -1273,7 +1273,7 @@
1.579 if (term2str t) =
1.580 "0"
1.581 then ()
1.582 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 20";
1.583 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 20";
1.584
1.585 (*Eigenes*)
1.586 val t = str2term
1.587 @@ -1283,7 +1283,7 @@
1.588 if (term2str t) =
1.589 "(3 * y + b * x) / (b * y)"
1.590 then ()
1.591 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 21";
1.592 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 21";
1.593
1.594
1.595 "-------- multiply and cancel ------------------------------------";
1.596 @@ -1298,7 +1298,7 @@
1.597 if (term2str t) =
1.598 "(5 * x + -5 * y) / (18 * x + 18 * y)"
1.599 then ()
1.600 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 22";
1.601 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 22";
1.602
1.603 (*SRM.test Schalk I, p.68 Nr. 436b *)
1.604 (*WN060420???MG3 crashes with method 'simplify' in
1.605 @@ -1309,26 +1309,26 @@
1.606 if (term2str t) =
1.607 "5 * a / (a + -1 * b)"
1.608 then ()
1.609 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
1.610 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
1.611
1.612 (*Schalk I, p.68 Nr. 437a *)
1.613 val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
1.614 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.615 if (term2str t) = "1 / (4 * c + 3 * e)" then ()
1.616 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1.617 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1.618
1.619 "----- S.K. corrected non-termination 060904";
1.620 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
1.621 val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1.622 if term2str t' = "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)" then ()
1.623 -else raise error "rational.sml.sml: S.K.8..corrected 060904-6";
1.624 +else error "rational.sml.sml: S.K.8..corrected 060904-6";
1.625
1.626 "----- S.K. corrected non-termination of cancel_p_";
1.627 val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
1.628 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
1.629 val SOME (t',_) = rewrite_set_ thy false cancel_p t'';
1.630 if term2str t' = "1 / (4 * c + 3 * e)" then ()
1.631 -else raise error "rational.sml.sml: diff.behav. in cancel_p S.K.8";
1.632 +else error "rational.sml.sml: diff.behav. in cancel_p S.K.8";
1.633
1.634 (**)
1.635
1.636 @@ -1354,7 +1354,7 @@
1.637 if (term2str t) =
1.638 "x ^^^ 2"
1.639 then ()
1.640 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1.641 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1.642
1.643 (*SRM Schalk I, p.68 Nr. 439b *)
1.644 val t = str2term
1.645 @@ -1364,7 +1364,7 @@
1.646 if (term2str t) =
1.647 "(x + -4 * x ^^^ 3) / 2"
1.648 then ()
1.649 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 25";
1.650 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 25";
1.651
1.652 (*SRM Schalk I, p.68 Nr. 440a *)
1.653 val t = str2term
1.654 @@ -1374,20 +1374,20 @@
1.655 if (term2str t) =
1.656 "(-3 + x) / (2 + x)"
1.657 then ()
1.658 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
1.659 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
1.660
1.661 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
1.662 val t = str2term
1.663 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
1.664 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.665 if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
1.666 -else raise error "rational.sml.sml: diff.behav. in norm_Rational 27";
1.667 +else error "rational.sml.sml: diff.behav. in norm_Rational 27";
1.668
1.669 "----- SK12 works since 0707xx";
1.670 val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
1.671 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.672 if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
1.673 -else raise error "rational.sml.sml: diff.behav. in norm_Rational 28";
1.674 +else error "rational.sml.sml: diff.behav. in norm_Rational 28";
1.675
1.676
1.677 "-------- common denominator and multiplication ------------------";
1.678 @@ -1406,7 +1406,7 @@
1.679 if (term2str t) =
1.680 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
1.681 then ()
1.682 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
1.683 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
1.684
1.685 (*SRAM Schalk I, p.69 Nr. 442b *)
1.686 val t = str2term "(15*a^^^2/x^^^3 - 5*b^^^4/x^^^2 + 25*c^^^2/x)*(x^^^3/(5*a*b^^^3*c^^^3)) + 1/c^^^3 * (b*x/a - 3*a/b^^^3)";
1.687 @@ -1415,7 +1415,7 @@
1.688 if (term2str t) =
1.689 "5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
1.690 then ()
1.691 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
1.692 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
1.693
1.694 (*SRAM Schalk I, p.69 Nr. 443b *)
1.695 val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
1.696 @@ -1424,7 +1424,7 @@
1.697 if (term2str t) =
1.698 "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
1.699 then ()
1.700 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
1.701 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
1.702
1.703 (*SRAM Schalk I, p.69 Nr. 445b *)
1.704 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
1.705 @@ -1433,7 +1433,7 @@
1.706 if (term2str t) =
1.707 "a ^^^ 3 / 27"
1.708 then ()
1.709 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
1.710 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
1.711
1.712 (*SRAM Schalk I, p.69 Nr. 446b *)
1.713 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
1.714 @@ -1442,7 +1442,7 @@
1.715 if (term2str t) =
1.716 "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
1.717 then ()
1.718 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
1.719 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
1.720
1.721 (*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1.722 val t = str2term
1.723 @@ -1452,7 +1452,7 @@
1.724 if (term2str t) =
1.725 "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1.726 then ()
1.727 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
1.728 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
1.729
1.730 (*SRAM Schalk I, p.69 Nr. 450a *)
1.731 val t = str2term
1.732 @@ -1462,7 +1462,7 @@
1.733 if (term2str t) =
1.734 "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
1.735 then ()
1.736 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
1.737 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
1.738
1.739 "-------- double fractions ---------------------------------------";
1.740 "-------- double fractions ---------------------------------------";
1.741 @@ -1476,7 +1476,7 @@
1.742 if (term2str t) =
1.743 "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
1.744 then ()
1.745 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
1.746 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
1.747
1.748 (*SRD Schalk I, p.69 Nr. 455a *)
1.749 val t = str2term
1.750 @@ -1485,26 +1485,26 @@
1.751 term2str t;
1.752 if (term2str t) =
1.753 "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
1.754 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
1.755 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
1.756
1.757
1.758 "----- Schalk I, p.69 Nr. 455b";
1.759 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
1.760 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.761 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
1.762 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
1.763 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
1.764
1.765 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
1.766 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
1.767 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.768 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
1.769 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37b";
1.770 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 37b";
1.771
1.772 "----- ?: worked before 0707xx";
1.773 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
1.774 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.775 if term2str t = "-1 / (3 + y)" then ()
1.776 -else raise error "rational.sml: -1 / (3 + y) norm_Rational";
1.777 +else error "rational.sml: -1 / (3 + y) norm_Rational";
1.778
1.779 (*SRD Schalk I, p.69 Nr. 456b *)
1.780 val t = str2term
1.781 @@ -1512,7 +1512,7 @@
1.782 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.783 term2str t;
1.784 if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
1.785 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
1.786 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
1.787
1.788 (*SRD Schalk I, p.69 Nr. 457b *)
1.789 val t = str2term
1.790 @@ -1522,20 +1522,20 @@
1.791 if (term2str t) =
1.792 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
1.793 then ()
1.794 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
1.795 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
1.796
1.797 "----- Schalk I, p.69 Nr. 458b works since 0707";
1.798 val t = str2term
1.799 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
1.800 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.801 if term2str t = "a ^^^ 2 / b ^^^ 2" then ()
1.802 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39b";
1.803 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 39b";
1.804
1.805 (*SRD Schalk I, p.69 Nr. 459b *)
1.806 val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
1.807 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.808 if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then ()
1.809 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
1.810 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
1.811
1.812
1.813 (*Schalk I, p.69 Nr. 460b nonterm.SK
1.814 @@ -1544,7 +1544,7 @@
1.815 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.816 if term2str t =
1.817 then ()
1.818 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
1.819 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
1.820
1.821 val t = str2term
1.822 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.823 @@ -1563,7 +1563,7 @@
1.824 if (term2str t) =
1.825 "x + y"
1.826 then ()
1.827 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
1.828 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
1.829
1.830
1.831 (*----------------------------------------------------------------------*)
1.832 @@ -1578,7 +1578,7 @@
1.833 if (term2str t) =
1.834 "1 / 2"
1.835 then ()
1.836 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
1.837 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
1.838
1.839 (*SRD Schalk I, p.69 Nr. 464b *)
1.840 val t = str2term
1.841 @@ -1588,7 +1588,7 @@
1.842 if (term2str t) =
1.843 "(3 + -1 * a) / (1 + -1 * a)"
1.844 then ()
1.845 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
1.846 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
1.847
1.848 (*SRD Schalk I, p.69 Nr. 465b *)
1.849 val t = str2term
1.850 @@ -1598,7 +1598,7 @@
1.851 if (term2str t) =
1.852 "(4 * x + 6 * y + -9 * z) / (4 * x)"
1.853 then ()
1.854 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
1.855 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
1.856
1.857 (*SRD Schalk I, p.69 Nr. 466b *)
1.858 val t = str2term
1.859 @@ -1608,7 +1608,7 @@
1.860 if (term2str t) =
1.861 "(25 + -10 * x + x ^^^ 2) / 18"
1.862 then ()
1.863 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
1.864 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
1.865
1.866 (*SRD Schalk I, p.70 Nr. 469 *)
1.867 val t = str2term
1.868 @@ -1618,7 +1618,7 @@
1.869 if (term2str t) =
1.870 "3 * b ^^^ 3 / (2 * a + -2 * b)"
1.871 then ()
1.872 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
1.873 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
1.874
1.875 (*----------------------------------------------------------------------*)
1.876 (*---------------------- Mehrfache Dppelbrueche ------------------------*)
1.877 @@ -1630,7 +1630,7 @@
1.878 "((a^^^2 - b^^^2)/(2*a*b)+2*a*b/(a^^^2 - b^^^2))/((a^^^2+b^^^2)/(2*a*b)+1) / ((a^^^2+b^^^2)^^^2/(a+b)^^^2)";
1.879 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.880 if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()
1.881 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
1.882 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
1.883
1.884 "----- Schalk I, p.70 Nr. 477a";
1.885 (* MG Achtung: terme explodieren; Bsp zu komplex;
1.886 @@ -1653,11 +1653,11 @@
1.887 if term2str t' =
1.888 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1.889 then ()
1.890 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
1.891 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
1.892
1.893 (* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
1.894 if term2str t' = "(a ^^^ 4 + -1 * a ^^^ 2 * b ^^^ 2) /\n(a * b * (b + (a * (a + -1 * b) + -1 * b * (a + -1 * b)) / (2 * a)) *\n (a + -1 * b))" then ()
1.895 -else raise error "rational.sml: works again";
1.896 +else error "rational.sml: works again";
1.897 re-outcommented with TODO.new_c: cvs before 071227, 11:50*)
1.898
1.899
1.900 @@ -1671,7 +1671,7 @@
1.901 if (term2str t) =
1.902
1.903 then ()
1.904 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
1.905 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
1.906
1.907 (*MG Berechne Zwischenergebnisse: WN060831 nonterm.SK00*)
1.908 val t = str2term
1.909 @@ -1751,7 +1751,7 @@
1.910 val t = str2term " (1 + x^^^5) / (y + x) + x^^^3 / x ";
1.911 val SOME (t,_) = rewrite_set_ thy false common_nominator_p t;
1.912 if term2str t = "(1 + x ^^^ 3 + x ^^^ 5 + y * x ^^^ 2) / (x + y)" then()
1.913 -else raise error "";
1.914 +else error "";
1.915
1.916 (*--------------------------------------------------------------------*)
1.917 (* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3b
1.918 @@ -1793,19 +1793,19 @@
1.919 val t = str2term "(a^^^2 + -1)/(a+1)";
1.920 val SOME (t',_) = rewrite_set_ thy false cancel_p t;
1.921 if term2str t' = "(-1 + a) / 1" then ()
1.922 -else raise error "rational.sml MG tests 3d";
1.923 +else error "rational.sml MG tests 3d";
1.924
1.925 "----- NOT TERMINATING ?: worked before 0707xx";
1.926 val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
1.927 val SOME (t'',_) = rewrite_set_ thy false norm_Rational t;
1.928 if term2str t'' = "(1 + -1 * a) / (1 + -1 * b)" then ()
1.929 -else raise error "rational.sml MG tests 3e";
1.930 +else error "rational.sml MG tests 3e";
1.931
1.932 "----- corrected SK060905";
1.933 val t = str2term "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
1.934 val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.935 if term2str t' = "-1 / (5 + -2 * x)" then ()
1.936 -else raise error "rational.sml corrected SK060905";
1.937 +else error "rational.sml corrected SK060905";
1.938
1.939
1.940 "--------------------------------------------------------------------";
1.941 @@ -1820,7 +1820,7 @@
1.942 if (term2str t) =
1.943 "5 * x ^^^ 2 / (b ^^^ 3 * c)"
1.944 then ()
1.945 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 53";
1.946 +else error "rational.sml.sml: diff.behav. in norm_Rational_mg 53";
1.947
1.948 "-------- me Schalk I No.186 -------------------------------------";
1.949 "-------- me Schalk I No.186 -------------------------------------";
1.950 @@ -1845,7 +1845,7 @@
1.951 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1.952 case (f2str f, nxt) of
1.953 ("14", ("End_Proof'", _)) => ()
1.954 - | _ => raise error "rational.sml diff.behav. in me Schalk I No.186";
1.955 + | _ => error "rational.sml diff.behav. in me Schalk I No.186";
1.956
1.957
1.958 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
1.959 @@ -1889,7 +1889,7 @@
1.960 val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);
1.961 (*if length newnds = 12 then () WN060905*)
1.962 if length newnds = 13 then ()
1.963 -else raise error "rational.sml: interSteps cancel_p rev_rew_p";
1.964 +else error "rational.sml: interSteps cancel_p rev_rew_p";
1.965
1.966 val p = ([2,1,9],Res);
1.967 getTactic 1 p;
1.968 @@ -1897,7 +1897,7 @@
1.969 (*case tac of SOME (Rewrite ("sym_real_plus_binom_times1", _)) => ()
1.970 WN060905*)
1.971 case tac of SOME (Rewrite ("sym_real_add_mult_distrib2", _)) => ()
1.972 -| _ => raise error "rational.sml: getTactic, sym_real_plus_binom_times1";
1.973 +| _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
1.974
1.975
1.976 "-------- investigate rulesets for cancel_p ----------------------";
1.977 @@ -1998,14 +1998,14 @@
1.978 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
1.979 val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.980 if term2str t' = "(2 + -1 * x) / (3 + y)" then ()
1.981 -else raise error "rational.sml SK060904-1a worked since 0707xx";
1.982 +else error "rational.sml SK060904-1a worked since 0707xx";
1.983
1.984 "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
1.985 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
1.986 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
1.987 val SOME (t',_) = cancel_p_ thy t;
1.988 if term2str t' = "1 / (4 * c + 3 * e)" then ()
1.989 -else raise error "rational.sml SK060904-1b";
1.990 +else error "rational.sml SK060904-1b";
1.991
1.992
1.993 "----- SK060904-2a non-termination of add_fraction_p_";
1.994 @@ -2027,14 +2027,14 @@
1.995 "-------- how to stepwise construct Scripts ----------------------";
1.996 "-------- how to stepwise construct Scripts ----------------------";
1.997 "-------- how to stepwise construct Scripts ----------------------";
1.998 -lse raise error "rational.sml SK060904-1a worked since 0707xx";
1.999 +lse error "rational.sml SK060904-1a worked since 0707xx";
1.1000
1.1001 "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
1.1002 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
1.1003 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
1.1004 val SOME (t',_) = cancel_p_ thy t;
1.1005 if term2str t' = "1 / (4 * c + 3 * e)" then ()
1.1006 -else raise error "rational.sml SK060904-1b";
1.1007 +else error "rational.sml SK060904-1b";
1.1008
1.1009
1.1010 "----- SK060904-2a non-termination of add_fraction_p_";
1.1011 @@ -2056,14 +2056,14 @@
1.1012 "-------- how to stepwise construct Scripts ----------------------";
1.1013 "-------- how to stepwise construct Scripts ----------------------";
1.1014 "-------- how to stepwise construct Scripts ----------------------";
1.1015 -lse raise error "rational.sml SK060904-1a worked since 0707xx";
1.1016 +lse error "rational.sml SK060904-1a worked since 0707xx";
1.1017
1.1018 "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
1.1019 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
1.1020 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
1.1021 val SOME (t',_) = cancel_p_ thy t;
1.1022 if term2str t' = "1 / (4 * c + 3 * e)" then ()
1.1023 -else raise error "rational.sml SK060904-1b";
1.1024 +else error "rational.sml SK060904-1b";
1.1025
1.1026
1.1027 "----- SK060904-2a non-termination of add_fraction_p_";