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.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)