test/Tools/isac/Knowledge/rootrateq.sml
branchisac-update-Isa09-2
changeset 37991 028442673981
parent 37960 ec20007095f2
child 38031 460c24a6a6ba
     1.1 --- a/test/Tools/isac/Knowledge/rootrateq.sml	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rootrateq.sml	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4  
     1.5  "--------------------- test thm rootrat_equation_left_1 ---------------------";
     1.6  val fmz = ["equality ( -2 + 1/(1 - sqrt(x))= 0)", "solveFor x","solutions L"];
     1.7 -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
     1.8 +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
     1.9  
    1.10  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.11  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.12 @@ -59,21 +59,21 @@
    1.13  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.14  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.15  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.16 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
    1.17 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
    1.18  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.19  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.20  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.21  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.22  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.23  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.24 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
    1.25 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
    1.26  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.27  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.28  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.29  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.30  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.31  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.32 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
    1.33 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
    1.34  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.35  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.36  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.37 @@ -82,7 +82,7 @@
    1.38  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.39  if f =  Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -4 * x = 0")) then ()
    1.40  else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_1";
    1.41 -(*-> Subproblem ("RootEq.thy", ["polynomial", ...])*)
    1.42 +(*-> Subproblem ("RootEq", ["polynomial", ...])*)
    1.43  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.44  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.45  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.46 @@ -98,7 +98,7 @@
    1.47  
    1.48  "--------------------- test thm rootrat_equation_left_2 ---------------------";
    1.49  val fmz = ["equality (3/(1+sqrt(x))= 1)", "solveFor x","solutions L"];
    1.50 -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
    1.51 +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
    1.52  
    1.53  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.54  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.55 @@ -106,21 +106,21 @@
    1.56  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.57  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.58  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.59 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
    1.60 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
    1.61  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.62  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.63  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.64  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.65  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.66  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.67 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
    1.68 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
    1.69  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.70  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.71  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.72  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.73  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.74  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.75 -(*-> Subproblem ("RootEq.thy", ["univariate", ...])*)
    1.76 +(*-> Subproblem ("RootEq", ["univariate", ...])*)
    1.77  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.78  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.79  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.80 @@ -129,7 +129,7 @@
    1.81  val (p,_,f,nxt,_,pt) = me nxt p c pt; 
    1.82  if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "4 + -1 * x = 0")) then ()
    1.83  else raise error "rootrateq.sml: diff.behav. in rootrat_equation_left_2";
    1.84 -(*-> Subproblem ("PolyEq.thy", ["polynomial", ...])*)
    1.85 +(*-> Subproblem ("PolyEq", ["polynomial", ...])*)
    1.86  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.87  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.88  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.89 @@ -145,7 +145,7 @@
    1.90  
    1.91  "--------------------- test thm rootrat_equation_right_1 ---------------";
    1.92  val fmz = ["equality ( 0= -2 + 1/(1 - sqrt(x)))", "solveFor x","solutions L"];
    1.93 -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
    1.94 +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
    1.95  
    1.96  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.97  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.98 @@ -188,7 +188,7 @@
    1.99  
   1.100  "--------------------- test thm rootrat_equation_right_2 --------------------";
   1.101  val fmz = ["equality (1 = 3/(1+sqrt(x)))", "solveFor x","solutions L"];
   1.102 -val (dI',pI',mI') = ("RootRatEq.thy",["univariate","equation"],["no_met"]);
   1.103 +val (dI',pI',mI') = ("RootRatEq",["univariate","equation"],["no_met"]);
   1.104  
   1.105  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
   1.106  val (p,_,f,nxt,_,pt) = me nxt p c pt; val (p,_,f,nxt,_,pt) = me nxt p c pt;