test/Tools/isac/Knowledge/rational.sml
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37980 c0a9d6bdc1d6
child 38031 460c24a6a6ba
     1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -472,7 +472,7 @@
     1.4  "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
     1.5  "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
     1.6  "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
     1.7 -val thy' = "Rational.thy";
     1.8 +val thy' = "Rational";
     1.9  val rls' = "cancel";
    1.10  val mp = "make_polynomial";
    1.11  
    1.12 @@ -1828,7 +1828,7 @@
    1.13  val fmz = ["TERM ((14 * x * y) / ( x * y ))",
    1.14  	   "normalform N"];
    1.15  val (dI',pI',mI') =
    1.16 -  ("Rational.thy",["rational","simplification"],
    1.17 +  ("Rational",["rational","simplification"],
    1.18     ["simplification","of_rationals"]);
    1.19  val p = e_pos'; val c = []; 
    1.20  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.21 @@ -1854,7 +1854,7 @@
    1.22  states:=[];
    1.23  CalcTree
    1.24  [(["TERM (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"], 
    1.25 -  ("Rational.thy",["rational","simplification"],
    1.26 +  ("Rational",["rational","simplification"],
    1.27    ["simplification","of_rationals"]))];
    1.28  Iterator 1;
    1.29  moveActiveRoot 1;
    1.30 @@ -1871,7 +1871,7 @@
    1.31  states:=[];
    1.32  CalcTree
    1.33  [(["TERM ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"], 
    1.34 -  ("Rational.thy",["rational","simplification"],
    1.35 +  ("Rational",["rational","simplification"],
    1.36    ["simplification","of_rationals"]))];
    1.37  Iterator 1;
    1.38  moveActiveRoot 1;