src/smltest/IsacKnowledge/rational.sml
branchstart-work-070517
changeset 262 5d65487829c7
parent 149 4ad61db2d257
     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