1.1 --- a/test/Tools/isac/Interpret/calchead.sml	Mon Oct 11 12:55:40 2010 +0200
     1.2 +++ b/test/Tools/isac/Interpret/calchead.sml	Mon Oct 11 13:31:22 2010 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  states := [];
     1.5   CalcTree
     1.6   [(["equality (x+1=2)", "solveFor x","solutions L"], 
     1.7 -   ("Test.thy", 
     1.8 +   ("Test", 
     1.9      ["sqroot-test","univariate","equation","test"],
    1.10      ["Test","squ-equ-test-subpbl1"]))];
    1.11   Iterator 1;
    1.12 @@ -73,7 +73,7 @@
    1.13       "interval {x::real. 0 <= x & x <= pi}",
    1.14       "errorBound (eps=(0::real))"];
    1.15  val (dI',pI',mI') =
    1.16 -  ("DiffApp.thy",["maximum_of","function"],
    1.17 +  ("DiffApp",["maximum_of","function"],
    1.18     ["DiffApp","max_by_calculus"]);
    1.19  val c = []:cid;
    1.20  
    1.21 @@ -167,7 +167,7 @@
    1.22       "interval {x::real. 0 <= x & x <= pi}",
    1.23       "errorBound (eps=(0::real))"];
    1.24  val (dI',pI',mI') =
    1.25 -  ("DiffApp.thy",["maximum_of","function"],
    1.26 +  ("DiffApp",["maximum_of","function"],
    1.27     ["DiffApp","max_by_calculus"]);
    1.28  val c = []:cid;
    1.29  (*val nxt = Init_Proof' (fmz,(dI',pI',mI'));*)
    1.30 @@ -210,7 +210,7 @@
    1.31  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.32  ------------------------------ FIXXXXME.meNEW !!! ---*)
    1.33  
    1.34 -(*val nxt = Specify_Theory "DiffApp.thy" : tac*)
    1.35 +(*val nxt = Specify_Theory "DiffApp" : tac*)
    1.36  
    1.37  val itms = get_obj g_pbl pt (fst p);writeln(itms2str_ ctxt itms);
    1.38  
    1.39 @@ -220,7 +220,7 @@
    1.40  
    1.41  val nxt = tac2tac_ pt p nxt; 
    1.42  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.43 -(*val nxt = Specify_Method ("DiffApp.thy","max_by_calculus")*)
    1.44 +(*val nxt = Specify_Method ("DiffApp","max_by_calculus")*)
    1.45  
    1.46  val nxt = tac2tac_ pt p nxt; 
    1.47  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.48 @@ -236,7 +236,7 @@
    1.49  
    1.50  val nxt = tac2tac_ pt p nxt; 
    1.51  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.52 -(*val nxt = Apply_Method ("DiffApp.thy","max_by_calculus") *)
    1.53 +(*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
    1.54  if nxt<>(Apply_Method ["DiffApp","max_by_calculus"])
    1.55  then error "test specify, fmz <> []: nxt <> Apply_Method max_by_calculus" else ();
    1.56  
    1.57 @@ -256,7 +256,7 @@
    1.58  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.59  (*val nxt = Specify_Theory "e_domID" : tac*)
    1.60  
    1.61 -val nxt = Specify_Theory "DiffApp.thy";
    1.62 +val nxt = Specify_Theory "DiffApp";
    1.63  val nxt = tac2tac_ pt p nxt; 
    1.64  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.65  (*val nxt = Specify_Problem ["e_pblID"] : tac*)
    1.66 @@ -315,13 +315,13 @@
    1.67  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt;
    1.68  (*val nxt = Apply_Method ("DiffApp","max_by_calculus") *)
    1.69  (*30.8.01 ... funktioniert nicht mehr nach Einfuehrung env ....
    1.70 -if nxt<>(Apply_Method ("DiffApp.thy","max_by_calculus"))
    1.71 +if nxt<>(Apply_Method ("DiffApp","max_by_calculus"))
    1.72  then error "test specify, fmz <> []: nxt <> Add_Relation.." 
    1.73  else ();
    1.74  *)
    1.75  
    1.76  (* 2.4.00 nach Transfer specify -> hard_gen
    1.77 -val nxt = Apply_Method ("DiffApp.thy","max_by_calculus");
    1.78 +val nxt = Apply_Method ("DiffApp","max_by_calculus");
    1.79  val(p,_,Form'(PpcKF(_,_,_,_,ppc)),nxt,_,pt) = specify nxt p [] pt; *)
    1.80  (*val nxt = Empty_Tac : tac*)
    1.81  
    1.82 @@ -602,7 +602,7 @@
    1.83         {env = None, fmz =
    1.84         (["functionTerm (x^^^2 + 1)", "integrateBy x",
    1.85  	 "antiDerivative FF"],
    1.86 -	("Integrate.thy", ["integrate", "function"],
    1.87 +	("Integrate", ["integrate", "function"],
    1.88  	 ["diff", "integration"])),
    1.89         loc =
    1.90         (Some (ScrState ([], [], None, Const ("empty", "'a"), Sundef, false)),
    1.91 @@ -624,7 +624,7 @@
    1.92  	 (3, [1], "#Find",
    1.93  	     Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
    1.94  	     [Free ("FF", "RealDef.real")])],
    1.95 -	("Integrate.thy", ["integrate", "function"], ["diff", "integration"]),
    1.96 +	("Integrate", ["integrate", "function"], ["diff", "integration"]),
    1.97  	Const ("Integrate.Integrate",
    1.98  	       "(RealDef.real, RealDef.real) * => RealDef.real") $
    1.99  	       (Const ("Pair",
   1.100 @@ -662,7 +662,7 @@
   1.101         {env = None, fmz =
   1.102         (["functionTerm (x^^^2 + 1)", "integrateBy x",
   1.103  	 "antiDerivative FF"],
   1.104 -	("Integrate.thy", ["integrate", "function"],
   1.105 +	("Integrate", ["integrate", "function"],
   1.106  	 ["diff", "integration"])),
   1.107         loc =
   1.108         (Some
   1.109 @@ -697,7 +697,7 @@
   1.110  	 (3, [1], "#Find",
   1.111  	     Const ("Integrate.antiDerivative", "RealDef.real => Tools.una"),
   1.112  	     [Free ("FF", "RealDef.real")])],
   1.113 -	("Integrate.thy", ["integrate", "function"], ["diff", "integration"]),
   1.114 +	("Integrate", ["integrate", "function"], ["diff", "integration"]),
   1.115  	Const ("Integrate.Integrate",
   1.116  	       "(RealDef.real, RealDef.real) * => RealDef.real") $
   1.117  	   (Const ("Pair",