test/Tools/isac/Knowledge/partial_fractions.sml
changeset 52103 0d13f07d8e2a
parent 48789 498ed5bb1004
child 52105 2786cc9704c8
     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