1.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Wed Sep 08 16:45:27 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Wed Sep 08 16:47:22 2010 +0200
     1.3 @@ -248,7 +248,7 @@
     1.4  val rls = "integration_rules";
     1.5  val subs = [("bdv","x::real")];
     1.6  fun rewrit_sinst subs rls str = 
     1.7 -    fst (the (rewrite_set_inst "Integrate.thy" true subs rls str));
     1.8 +    fst (the (rewrite_set_inst "Integrate" true subs rls str));
     1.9  (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.10  val str = rewrit_sinst subs rls "Integral x D x";
    1.11  val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
    1.12 @@ -362,16 +362,16 @@
    1.13  "----------- check Scripts ---------------------------------------";
    1.14  "----------- check Scripts ---------------------------------------";
    1.15  val str = 
    1.16 -"Script IntegrationScript (f_::real) (v_::real) =               \
    1.17 +"Script IntegrationScript (f_::real) (v_v::real) =               \
    1.18  \  (let t_ = Take (Integral f_ D v_v)                                 \
    1.19 -\   in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))";
    1.20 +\   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))";
    1.21  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.22  atomty sc;
    1.23  
    1.24  val str = 
    1.25 -"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = \
    1.26 +"Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = \
    1.27  \  (let t_ = Take (F_ v_v = Integral f_ D v_v)                         \
    1.28 -\   in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)";
    1.29 +\   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)";
    1.30  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.31  atomty sc;
    1.32  show_mets();
    1.33 @@ -384,7 +384,7 @@
    1.34  val fmz = ["functionTerm (x^^^2 + 1)", 
    1.35  	   "integrateBy x","antiDerivative FF"];
    1.36  val (dI',pI',mI') =
    1.37 -  ("Integrate.thy",["integrate","function"],
    1.38 +  ("Integrate",["integrate","function"],
    1.39     ["diff","integration"]);
    1.40  val p = e_pos'; val c = []; 
    1.41  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.42 @@ -409,7 +409,7 @@
    1.43  val fmz = ["functionTerm (x^^^2 + 1)", 
    1.44  	   "integrateBy x","antiDerivativeName F"];
    1.45  val (dI',pI',mI') =
    1.46 -  ("Integrate.thy",["named","integrate","function"],
    1.47 +  ("Integrate",["named","integrate","function"],
    1.48     ["diff","integration","named"]);
    1.49  val p = e_pos'; val c = []; 
    1.50  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.51 @@ -434,7 +434,7 @@
    1.52  val fmz = ["functionTerm (- q_0)", 
    1.53  	   "integrateBy x","antiDerivativeName Q"];
    1.54  val (dI',pI',mI') =
    1.55 -  ("Biegelinie.thy",["named","integrate","function"],
    1.56 +  ("Biegelinie",["named","integrate","function"],
    1.57     ["diff","integration","named"]);
    1.58  val p = e_pos'; val c = [];
    1.59  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
    1.60 @@ -460,7 +460,7 @@
    1.61  states:=[];
    1.62  CalcTree
    1.63  [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"], 
    1.64 -  ("Integrate.thy",["integrate","function"],
    1.65 +  ("Integrate",["integrate","function"],
    1.66    ["diff","integration"]))];
    1.67  Iterator 1;
    1.68  moveActiveRoot 1;
    1.69 @@ -486,17 +486,17 @@
    1.70  		srls = e_rls, 
    1.71  		prls=e_rls,
    1.72  	     crls = Atools_erls, nrls = e_rls},
    1.73 -"Script IntegrationScript (f_::real) (v_::real) =             \
    1.74 -\  (((Rewrite_Set_Inst [(bdv,v_)] integration_rules False) @@ \
    1.75 -\    (Rewrite_Set_Inst [(bdv,v_)] add_new_c False)         @@ \
    1.76 -\    (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) (f_::real))"
    1.77 +"Script IntegrationScript (f_::real) (v_v::real) =             \
    1.78 +\  (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \
    1.79 +\    (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False)         @@ \
    1.80 +\    (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_::real))"
    1.81  ));
    1.82  
    1.83  states:=[];
    1.84  CalcTree
    1.85  [(["functionTerm (Integral x^2 + 1 D x)","integrateBy x",
    1.86     "antiDerivative FF"], 
    1.87 -  ("Integrate.thy",["integrate","function"],
    1.88 +  ("Integrate",["integrate","function"],
    1.89    ["diff","integration","test"]))];
    1.90  Iterator 1;
    1.91  moveActiveRoot 1;
    1.92 @@ -527,7 +527,7 @@
    1.93  states:=[];
    1.94  CalcTree
    1.95  [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"], 
    1.96 -  ("Integrate.thy",["integrate","function"],
    1.97 +  ("Integrate",["integrate","function"],
    1.98    ["diff","integration"]))];
    1.99  Iterator 1;
   1.100  moveActiveRoot 1;