test/Tools/isac/Knowledge/partial_fractions.sml
changeset 48789 498ed5bb1004
parent 48761 4162c4f6f897
child 52103 0d13f07d8e2a
     1.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml	Wed Dec 05 10:21:35 2012 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Wed Dec 05 15:29:36 2012 +0100
     1.3 @@ -91,8 +91,8 @@
     1.4  val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
     1.5  
     1.6  val test = HOLogic.mk_binop "Groups.plus_class.plus"
     1.7 -  (HOLogic.mk_binop "Rings.inverse_class.divide" (A_var, denom1),
     1.8 -   HOLogic.mk_binop "Rings.inverse_class.divide" (B_var, denom2));
     1.9 +  (HOLogic.mk_binop "Fields.inverse_class.divide" (A_var, denom1),
    1.10 +   HOLogic.mk_binop "Fields.inverse_class.divide" (B_var, denom2));
    1.11  
    1.12  if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
    1.13    else error "HOLogic.mk_binop broken ?";