1.1 --- a/src/smltest/IsacKnowledge/rational.sml Mon Dec 10 14:18:49 2007 +0100
1.2 +++ b/src/smltest/IsacKnowledge/rational.sml Thu Dec 27 12:25:27 2007 +0100
1.3 @@ -1649,15 +1649,15 @@
1.4 val t = str2term "(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / \
1.5 \((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
1.6 val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.7 -(* WN050820 was OK until STOP_REW_SUB introduced -- the ONLY change !!!
1.8 - ????SK ???MG
1.9 if term2str t' =
1.10 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1.11 then ()
1.12 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
1.13 ------------------------------------------------------------------------*)
1.14 +
1.15 +(* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
1.16 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.17 else raise error "rational.sml: works again";
1.18 +re-outcommented with TODO.new_c: cvs before 071227, 11:50*)
1.19
1.20
1.21