1.1 --- a/src/smltest/IsacKnowledge/rational.sml Tue Sep 05 16:06:48 2006 +0200
1.2 +++ b/src/smltest/IsacKnowledge/rational.sml Tue Sep 05 16:46:29 2006 +0200
1.3 @@ -1408,7 +1408,7 @@
1.4 then ()
1.5 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
1.6
1.7 -(*Schalk I, p.68 Nr. 440b *)
1.8 +"----- Schalk I, p.68 Nr. 440b";
1.9 (* Achtung: rechnet ewig; cancel_p hängt sich auf... WN060831????SK11
1.10 val t = str2term
1.11 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
1.12 @@ -1435,103 +1435,73 @@
1.13 "-------- common denominator and multiplication ------------------";
1.14 "-------- common denominator and multiplication ------------------";
1.15 "-------- common denominator and multiplication ------------------";
1.16 -
1.17 (*----------------------------------------------------------------------*)
1.18 (*--------- Gemeinsamer Nenner und Multiplikation von Brüchen ----------*)
1.19 (*----------------------------------------------------------------------*)
1.20
1.21 -
1.22 -(*SRAM Schalk I, p.69 Nr. 441b *)
1.23 +"----- SRAM Schalk I, p.69 Nr. 441b";
1.24 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))";
1.25 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.26 -term2str t;
1.27 if (term2str t) =
1.28 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
1.29 -then ()
1.30 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
1.31 +then() else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
1.32
1.33 -(*SRAM Schalk I, p.69 Nr. 442b *)
1.34 +"----- SRAM Schalk I, p.69 Nr. 442b";
1.35 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.36 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.37 -term2str t;
1.38 -if (term2str t) =
1.39 -"5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
1.40 -then ()
1.41 +if (term2str t) = "5 * x ^^^ 2 / (a * b ^^^ 3 * c)" then ()
1.42 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
1.43
1.44 -(*SRAM Schalk I, p.69 Nr. 443b *)
1.45 +"----- SRAM Schalk I, p.69 Nr. 443b";
1.46 val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
1.47 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.48 -term2str t;
1.49 -if (term2str t) =
1.50 -"(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
1.51 -then ()
1.52 +if (term2str t) ="(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36" then ()
1.53 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
1.54
1.55 -(*SRAM Schalk I, p.69 Nr. 445b *)
1.56 +"----- SRAM Schalk I, p.69 Nr. 445b";
1.57 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
1.58 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.59 -term2str t;
1.60 -if (term2str t) =
1.61 -"a ^^^ 3 / 27"
1.62 -then ()
1.63 +if (term2str t) = "a ^^^ 3 / 27" then ()
1.64 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
1.65
1.66 -(*SRAM Schalk I, p.69 Nr. 446b *)
1.67 +"----- SRAM Schalk I, p.69 Nr. 446b";
1.68 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
1.69 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.70 -term2str t;
1.71 -if (term2str t) =
1.72 -"30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
1.73 -then ()
1.74 +if (term2str t) = "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2" then ()
1.75 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
1.76
1.77 -(*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1.78 +"----- SRAM Schalk I, p.69 Nr. 449a Achtung: rechnet ca 8 Sekunden";
1.79 val t = str2term
1.80 "(2*x^^^2/(3*y)+x/y^^^2)*(4*x^^^4/(9*y^^^2)+x^^^2/y^^^4)*(2*x^^^2/(3*y) - x/y^^^2)";
1.81 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.82 -term2str t;
1.83 -if (term2str t) =
1.84 -"(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1.85 -then ()
1.86 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
1.87 +if (term2str t) = "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1.88 +then() else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
1.89
1.90 -(*SRAM Schalk I, p.69 Nr. 450a *)
1.91 +"----- SRAM Schalk I, p.69 Nr. 450a";
1.92 val t = str2term
1.93 "(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
1.94 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.95 -term2str t;
1.96 -if (term2str t) =
1.97 -"(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
1.98 -then ()
1.99 +if (term2str t) = "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)" then ()
1.100 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
1.101
1.102 "-------- double fractions ---------------------------------------";
1.103 "-------- double fractions ---------------------------------------";
1.104 "-------- double fractions ---------------------------------------";
1.105
1.106 -(*SRD Schalk I, p.69 Nr. 454b *)
1.107 -val t = str2term
1.108 -"((2 - x)/(2*a)) / (2*a/(x - 2))";
1.109 +"----- SRD Schalk I, p.69 Nr. 454b";
1.110 +val t = str2term "((2 - x)/(2*a)) / (2*a/(x - 2))";
1.111 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.112 -term2str t;
1.113 -if (term2str t) =
1.114 -"(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
1.115 -then ()
1.116 +if (term2str t) = "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)" then ()
1.117 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
1.118
1.119 -(*SRD Schalk I, p.69 Nr. 455a *)
1.120 -val t = str2term
1.121 -"(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
1.122 +"----- SRD Schalk I, p.69 Nr. 455a";
1.123 +val t = str2term "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
1.124 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.125 -term2str t;
1.126 -if (term2str t) =
1.127 -"(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)"
1.128 -then ()
1.129 +if (term2str t) = "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
1.130 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
1.131
1.132
1.133 -(*Schalk I, p.69 Nr. 455b *)
1.134 +"----- Schalk I, p.69 Nr. 455b";
1.135 (* Achtung: Endlosschleife
1.136 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
1.137 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.138 @@ -1564,27 +1534,21 @@
1.139 (*MG: -1 im Zähler der Angabe verursacht das Problem ! WN060831???MG!!SK0*)
1.140 *)
1.141
1.142 -(*SRD Schalk I, p.69 Nr. 456b *)
1.143 -val t = str2term
1.144 -"(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
1.145 +"----- SRD Schalk I, p.69 Nr. 456b";
1.146 +val t = str2term "(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
1.147 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.148 -term2str t;
1.149 -if (term2str t) =
1.150 -"b / (1 + 2 * b + b ^^^ 2)"
1.151 -then ()
1.152 +if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
1.153 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
1.154
1.155 -(*SRD Schalk I, p.69 Nr. 457b *)
1.156 +"----- SRD Schalk I, p.69 Nr. 457b";
1.157 val t = str2term
1.158 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))";
1.159 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.160 -term2str t;
1.161 if (term2str t) =
1.162 -"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
1.163 -then ()
1.164 +"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2" then ()
1.165 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
1.166
1.167 -(*Schalk I, p.69 Nr. 458b *)
1.168 +"----- Schalk I, p.69 Nr. 458b";
1.169 (* Achtung: rechnet ewig; cancel_p hängt sich auf... ????SK
1.170 val t = str2term
1.171 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
1.172 @@ -1596,45 +1560,36 @@
1.173 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 40";
1.174 *)
1.175
1.176 -(*SRD Schalk I, p.69 Nr. 459b *)
1.177 -val t = str2term
1.178 -"(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
1.179 +"----- SRD Schalk I, p.69 Nr. 459b";
1.180 +val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
1.181 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.182 -term2str t;
1.183 -if (term2str t) =
1.184 -"(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)"
1.185 -then ()
1.186 +if (term2str t) = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)"then ()
1.187 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
1.188
1.189 -
1.190 -(*Schalk I, p.69 Nr. 460b *)
1.191 -(* Achtung: rechnet ewig; cancel_p hängt sich auf... ????SK
1.192 +"----- Schalk I, p.69 Nr. 460b";
1.193 +(* Achtung: rechnet ewig; cancel_p hängt sich auf... ????SK*)
1.194 val t = str2term
1.195 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1.196 +(*
1.197 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.198 -term2str t;
1.199 if (term2str t) =
1.200 -
1.201 then ()
1.202 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
1.203 -
1.204 +*)
1.205 val t = str2term
1.206 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.207 -val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1.208 +val Some (t',_) = rewrite_set_ thy false make_polynomial t;
1.209 +term2str t' = "(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y +\n 144 * x ^^^ 2 * y) /\n(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)";
1.210 +(* ????SK NOT terminating
1.211 +val Some (t'',_) = rewrite_set_ thy false cancel_p t';
1.212 term2str t;
1.213 -"(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y) /(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)";
1.214 -val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.215 -term2str t;
1.216 - ????SK*)
1.217 +*)
1.218
1.219 -(*SRD Schalk I, p.70 Nr. 472a *)
1.220 +"----- SRD Schalk I, p.70 Nr. 472a";
1.221 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
1.222 \((4*x - 8*y)/(x + y))";
1.223 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.224 -term2str t;
1.225 -if (term2str t) =
1.226 -"x + y"
1.227 -then ()
1.228 +if (term2str t) = "x + y" then ()
1.229 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
1.230
1.231
1.232 @@ -1642,54 +1597,36 @@
1.233 (*---------------------- Einfache Dppelbrüche --------------------------*)
1.234 (*----------------------------------------------------------------------*)
1.235
1.236 -(*SRD Schalk I, p.69 Nr. 461a *)
1.237 -val t = str2term
1.238 -"(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
1.239 +"----- Schalk I, p.69 Nr. 461a";
1.240 +val t = str2term "(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
1.241 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.242 -term2str t;
1.243 -if (term2str t) =
1.244 -"1 / 2"
1.245 -then ()
1.246 +if (term2str t) = "1 / 2" then ()
1.247 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
1.248
1.249 -(*SRD Schalk I, p.69 Nr. 464b *)
1.250 -val t = str2term
1.251 -"(a - a/(a - 2)) / (a + a/(a - 2))";
1.252 +"----- SRD Schalk I, p.69 Nr. 464b";
1.253 +val t = str2term "(a - a/(a - 2)) / (a + a/(a - 2))";
1.254 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.255 -term2str t;
1.256 -if (term2str t) =
1.257 -"(3 + -1 * a) / (1 + -1 * a)"
1.258 -then ()
1.259 +if (term2str t) = "(3 + -1 * a) / (1 + -1 * a)" then ()
1.260 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
1.261
1.262 -(*SRD Schalk I, p.69 Nr. 465b *)
1.263 -val t = str2term
1.264 -"((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
1.265 +"----- SRD Schalk I, p.69 Nr. 465b";
1.266 +val t = str2term "((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
1.267 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.268 -term2str t;
1.269 -if (term2str t) =
1.270 -"(4 * x + 6 * y + -9 * z) / (4 * x)"
1.271 -then ()
1.272 +if (term2str t) = "(4 * x + 6 * y + -9 * z) / (4 * x)" then ()
1.273 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
1.274
1.275 -(*SRD Schalk I, p.69 Nr. 466b *)
1.276 +"-----SRD Schalk I, p.69 Nr. 466b";
1.277 val t = str2term
1.278 "((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
1.279 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.280 -term2str t;
1.281 -if (term2str t) =
1.282 -"(25 + -10 * x + x ^^^ 2) / 18"
1.283 -then ()
1.284 +if (term2str t) = "(25 + -10 * x + x ^^^ 2) / 18" then ()
1.285 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
1.286
1.287 -(*SRD Schalk I, p.70 Nr. 469 *)
1.288 +"-----SRD Schalk I, p.70 Nr. 469";
1.289 val t = str2term
1.290 "3*b^^^2/(4*a^^^2 - 8*a*b + 4*b^^^2)/(a/(a^^^2*b - b^^^3) + (a - b)/(4*a*b^^^2+4*b^^^3) - 1/(4*b^^^2))";
1.291 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.292 -term2str t;
1.293 -if (term2str t) =
1.294 -"3 * b ^^^ 3 / (2 * a + -2 * b)"
1.295 -then ()
1.296 +if (term2str t) = "3 * b ^^^ 3 / (2 * a + -2 * b)" then ()
1.297 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
1.298
1.299 (*----------------------------------------------------------------------*)
1.300 @@ -1707,7 +1644,7 @@
1.301 then ()
1.302 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
1.303
1.304 -(*Schalk I, p.70 Nr. 477a *)
1.305 +"----- Schalk I, p.70 Nr. 477a";
1.306 (* Achtung: rechnet ewig; Bsp zu komplex;
1.307 Lösung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
1.308 val t = str2term "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /\
1.309 @@ -1727,23 +1664,24 @@
1.310 /\n(a ^^^ 2 * b ^^^ 5 * y + -1 * a ^^^ 2 * b ^^^ 4 * y ^^^ 2 +\n -3 * a ^^^ 2 * b ^^^ 3 * y ^^^ 3 +\n a ^^^ 2 * b ^^^ 2 * y ^^^ 4 +\n 2 * a ^^^ 2 * b * y ^^^ 5 +\n 2 * a * b ^^^ 5 * x * y +\n -2 * a * b ^^^ 4 * x * y ^^^ 2 +\n -6 * a * b ^^^ 3 * x * y ^^^ 3 +\n 2 * a * b ^^^ 2 * x * y ^^^ 4 +\n 4 * a * b * x * y ^^^ 5 +\n b ^^^ 5 * x ^^^ 2 * y +\n -1 * b ^^^ 4 * x ^^^ 2 * y ^^^ 2 +\n -3 * b ^^^ 3 * x ^^^ 2 * y ^^^ 3 +\n b ^^^ 2 * x ^^^ 2 * y ^^^ 4 +\n 2 * b * x ^^^ 2 * y ^^^ 5)";
1.311 *)
1.312
1.313 -(*Schalk I, p.70 Nr. 478b *) (* Rechenzeit: 5 sec *)
1.314 +"----- Schalk I, p.70 Nr. 478b *) (* Rechenzeit: 5 sec";
1.315 val t = str2term "(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / \
1.316 \((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
1.317 val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.318 term2str t';
1.319 (* WN050820 was OK until STOP_REW_SUB introduced -- the ONLY change !!!
1.320 - ????SK ???MG
1.321 + ???MG
1.322 if term2str t' =
1.323 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1.324 then ()
1.325 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
1.326 ------------------------------------------------------------------------*)
1.327 +*)
1.328
1.329 (*Schalk I, p.70 Nr. 480a *)
1.330 -(* SK Achtung: rechnet ewig; cancel_p kann nicht kürzen: WN060831????SK00
1.331 +(* WN060831????SK NOT terminating*)
1.332 val t = str2term
1.333 "(1/x+1/y+1/z)/(1/x - 1/y - 1/z) / (2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z)))";
1.334 +(*
1.335 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.336 term2str t;
1.337 if (term2str t) =
1.338 @@ -1776,18 +1714,13 @@
1.339 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.340 term2str t;
1.341 (*uncaught exception nonexhaustive binding failure*)
1.342 +*)
1.343
1.344 -(* Das kann er aber kürzen !!????: *)
1.345 +(*MG Das kann er aber kürzen !!????: *)
1.346 val t = str2term
1.347 "(x^^^2 * (y^^^2 * z) + x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
1.348 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.349 -term2str t;
1.350 -"(-1 * (y * x) + -1 * (z * y)) / (1 * (z * x) + -1 * (z * y))";
1.351 -*)
1.352 -
1.353 -
1.354 -
1.355 -
1.356 +term2str t = "(-1 * (y * x) + -1 * (z * y)) / (z * x + -1 * (z * y))";
1.357
1.358
1.359 (*--------------------------------------------------------------------*)
1.360 @@ -1882,17 +1815,10 @@
1.361 (* -1 im Zähler der Angabe verursacht das Problem !*)
1.362 *)
1.363
1.364 -(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
1.365 -(*Eigenes*)
1.366 -(* Achtung: Endlosschleife bei cancel_p:
1.367 +"----- corrected SK060905";
1.368 val t = str2term "(a^^^2 + -1)/(a+1)";
1.369 -val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1.370 -term2str t;
1.371 -"(-1 + a^^^2) / (1 + a)";
1.372 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.373 -term2str t;
1.374 -"(-1 + 1 * a) / 1"; (*OK*)
1.375 -*)
1.376 +term2str t = "(-1 + a) / 1";
1.377
1.378 "----- NOT TERMINATING";
1.379 val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";