1.1 --- a/src/smltest/IsacKnowledge/rational.sml Tue Sep 05 16:54:36 2006 +0200
1.2 +++ b/src/smltest/IsacKnowledge/rational.sml Tue Sep 05 17:06:37 2006 +0200
1.3 @@ -1368,21 +1368,18 @@
1.4 (*Schalk I, p.68 Nr. 437b *)
1.5 (* SK loops, Falsches Ergebnis: cancel_p kann nicht weiter krzen!!! *)
1.6 val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1.7 +(*
1.8 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.9 term2str t; WN060831????SK9
1.10 "(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
1.11 -
1.12 -(**)
1.13 +*)
1.14
1.15 (* *)
1.16 val t = str2term
1.17 "(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
1.18 -(* WN060831????SK10 *)
1.19 +(* WN060831????SK10
1.20 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.21 term2str t;
1.22 -(*
1.23 -uncaught exception nonexhaustive binding failure
1.24 - raised at: stdIn:270.1-270.51
1.25 *)
1.26
1.27 (*SRM Schalk I, p.68 Nr. 438a *)