1.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Fri Sep 13 18:57:11 2013 +0200
1.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Mon Sep 16 10:46:51 2013 +0200
1.3 @@ -322,9 +322,9 @@
1.4 term2str t'' = "(z - 1 / 2) * (z - -1 / 4) * 3 / ((-1 + -2 * z + 8 * z ^^^ 2) * 3 / 24) =\n" ^
1.5 "?A * (z - -1 / 4) + ?B * (z - 1 / 2)"; (*true*)
1.6
1.7 -val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
1.8 -if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then ()
1.9 -else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
1.10 +val SOME (t''', _) = rewrite_set_ @{theory Isac} true norm_Rational t'';
1.11 +if term2str t''' = "3 = ?A * (1 + 4 * z) / 4 + ?B * (-1 + 2 * z) / 2" then ()
1.12 +else error "ansatz_rls - multiply_ansatz - norm_Rational broken";
1.13
1.14 (*test for outcommented 3 lines in script: empower erls for x = a*b ==> ...*)
1.15 val xxx = append_rls "multiply_ansatz_erls" norm_Rational