1.1 --- a/test/Tools/isac/Knowledge/rateq.sml	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rateq.sml	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4  (* refine fmz ["univariate","equation"];
     1.5     *)
     1.6  
     1.7 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
     1.8 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
     1.9  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.10  (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.11     --------------------------------------- Refine_Tacitly*)
    1.12 @@ -56,7 +56,7 @@
    1.13  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.14  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.15  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.16 -(* val nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"])*)
    1.17 +(* val nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"])*)
    1.18  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.19  (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.20     --------------------------------------- Refine_Tacitly*)
    1.21 @@ -73,7 +73,7 @@
    1.22  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.23  (**** assoc_thm': 'all_left' not in 'RatEq.thy' (and parents)*)
    1.24  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.25 -(* val nxt = ("Subproblem",  Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
    1.26 +(* val nxt = ("Subproblem",  Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
    1.27  
    1.28  
    1.29  
    1.30 @@ -104,7 +104,7 @@
    1.31  (* refine fmz ["univariate","equation"];
    1.32  *)
    1.33  
    1.34 -val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],["no_met"]);
    1.35 +val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
    1.36  (*val p = e_pos'; 
    1.37  val c = []; 
    1.38  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
    1.39 @@ -118,7 +118,7 @@
    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 -(* nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"]))*)
    1.44 +(* nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"]))*)
    1.45  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.46  (* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","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 @@ -127,7 +127,7 @@
    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;
    1.52 -(* ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])) *)
    1.53 +(* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *)
    1.54  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
    1.55  (* nxt = ("Model_Problem", Model_Problem
    1.56       ["abcFormula","degree_2","polynomial","univariate","equation"])*)