test/Tools/isac/Knowledge/rational.sml
branchdecompose-isar
changeset 41932 a5e894d9fd8a
parent 41931 ca6aac81b893
child 41933 8d38adf87848
     1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Thu Mar 17 10:11:18 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Thu Mar 17 10:46:02 2011 +0100
     1.3 @@ -1343,8 +1343,11 @@
     1.4  "----- S.K. corrected non-termination 060904";
     1.5  val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
     1.6  val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
     1.7 -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.8 -else error "rational.sml: S.K.8..corrected 060904-6";
     1.9 +term2str t';
    1.10 +if term2str t' = 
    1.11 +  "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)"
    1.12 +(*"(9 * a ^^^ 2 + -16 * b ^^^ 2) / (36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)"*)
    1.13 +then () else error "rational.sml: S.K.8..corrected 060904-6";
    1.14  
    1.15  "----- S.K. corrected non-termination of cancel_p_";
    1.16  val t'' = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
    1.17 @@ -1420,7 +1423,7 @@
    1.18  val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
    1.19  term2str t;
    1.20  if (term2str t) =
    1.21 -"(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 +\n 16 * a ^^^ 4 * b) /\n(9 * a ^^^ 4)"
    1.22 +  "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
    1.23  then () else error "rational.sml: diff.behav. in norm_Rational_mg 28";
    1.24  
    1.25  (*SRAM Schalk I, p.69 Nr. 442b *)
    1.26 @@ -1531,10 +1534,8 @@
    1.27  val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
    1.28  term2str t;
    1.29  if (term2str t) = 
    1.30 -(*"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"*)
    1.31 -"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b +\n9 * a * b ^^^ 2"
    1.32 -then ()
    1.33 -else error "rational.sml: diff.behav. in norm_Rational_mg 39";
    1.34 +  "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
    1.35 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 39";
    1.36  
    1.37  "----- Schalk I, p.69 Nr. 458b works since 0707";
    1.38  val t = str2term 
    1.39 @@ -2077,3 +2078,5 @@
    1.40  "    Try (Rewrite_Set discard_parentheses False))               " ^
    1.41  "   t_t)"
    1.42  );
    1.43 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.44 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)