1.1 --- a/test/Tools/isac/Knowledge/rlang.sml	Wed Sep 08 10:15:51 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rlang.sml	Wed Sep 08 12:10:43 2010 +0200
     1.3 @@ -951,13 +951,13 @@
     1.4  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
     1.5  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
     1.6  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
     1.7 -(* val nxt = ("Model_Problem",Model_Problem ["normalize","root","univariate","equation"])*)
     1.8 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
     1.9 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.10 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.11 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.12 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.13 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
    1.14 +(* val nxt = ("Model_Problem",Model_Problem ["normalize","root'","univariate","equation"])*)
    1.15 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.16 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.17 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.18 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.19 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.20 +(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
    1.21  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.22  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.23  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.24 @@ -965,7 +965,7 @@
    1.25  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.26  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.27  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.28 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
    1.29 +(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
    1.30  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.31  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.32  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.33 @@ -1133,15 +1133,15 @@
    1.34  val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
    1.35  
    1.36  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.37 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
    1.38 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.39 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.40 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.41 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.42 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.43 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.44 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.45 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
    1.46 +(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
    1.47 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.48 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.49 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.50 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.51 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.52 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.53 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.54 +(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
    1.55  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.56  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.57  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.58 @@ -1150,7 +1150,7 @@
    1.59  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.60  val (p,_,f,nxt,_,pt) = me nxt p [1] pt; f2str f;
    1.61  val (p,_,f,nxt,_,pt) = me nxt p [1] pt; 
    1.62 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
    1.63 +(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
    1.64  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.65  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.66  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.67 @@ -1598,15 +1598,15 @@
    1.68  val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
    1.69  
    1.70  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.71 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"])*)
    1.72 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.73 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.74 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.75 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.76 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.77 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.78 -val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.79 -(* val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"])*)
    1.80 +(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"])*)
    1.81 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.82 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.83 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.84 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.85 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.86 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.87 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.88 +(* val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"])*)
    1.89  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.90  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.91  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.92 @@ -1659,7 +1659,7 @@
    1.93  	   "solveFor x","solutions L"];
    1.94  val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],["no_met"]);
    1.95  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.96 -(*val nxt = ("Model_Problem",Model_Problem ["sq","root","univariate","equation"]) *)
    1.97 +(*val nxt = ("Model_Problem",Model_Problem ["sq","root'","univariate","equation"]) *)
    1.98  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.99  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   1.100  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   1.101 @@ -1818,7 +1818,7 @@
   1.102  val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],["no_met"]);
   1.103  
   1.104  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
   1.105 -(*   Model_Problem ["normalize","root","univariate","equation"])*)
   1.106 +(*   Model_Problem ["normalize","root'","univariate","equation"])*)
   1.107  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
   1.108  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
   1.109  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
   1.110 @@ -1827,7 +1827,7 @@
   1.111  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
   1.112  (*val nxt = Subproblem ("RootEq.thy",["univariate","equation"]))*)
   1.113  val (p,_,f,nxt,_,pt) = me nxt p c pt;
   1.114 -(*val nxt = Model_Problem ["sq","root","univariate","equation"]) *)
   1.115 +(*val nxt = Model_Problem ["sq","root'","univariate","equation"]) *)
   1.116  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
   1.117  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
   1.118  val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;