test/Tools/isac/Knowledge/integrate.sml
branchisac-update-Isa09-2
changeset 37994 eb4c556a525b
parent 37991 028442673981
child 38010 a37a3ab989f4
     1.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Wed Sep 08 17:17:29 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Wed Sep 08 17:20:03 2010 +0200
     1.3 @@ -314,7 +314,7 @@
     1.4  "----------- check probem type -----------------------------------";
     1.5  "----------- check probem type -----------------------------------";
     1.6  "----------- check probem type -----------------------------------";
     1.7 -val model = {Given =["functionTerm f_", "integrateBy v_v"],
     1.8 +val model = {Given =["functionTerm f_f", "integrateBy v_v"],
     1.9  	     Where =[],
    1.10  	     Find  =["antiDerivative F_"],
    1.11  	     With  =[],
    1.12 @@ -326,7 +326,7 @@
    1.13  case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
    1.14  	 | _ => raise error "integrate.sml: Integrate.antiDerivative ???";
    1.15  
    1.16 -val model = {Given =["functionTerm f_", "integrateBy v_v"],
    1.17 +val model = {Given =["functionTerm f_f", "integrateBy v_v"],
    1.18  	     Where =[],
    1.19  	     Find  =["antiDerivativeName F_"],
    1.20  	     With  =[],
    1.21 @@ -362,14 +362,14 @@
    1.22  "----------- check Scripts ---------------------------------------";
    1.23  "----------- check Scripts ---------------------------------------";
    1.24  val str = 
    1.25 -"Script IntegrationScript (f_::real) (v_v::real) =               \
    1.26 +"Script IntegrationScript (f_f::real) (v_v::real) =               \
    1.27  \  (let t_ = Take (Integral f_ D v_v)                                 \
    1.28  \   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))";
    1.29  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.30  atomty sc;
    1.31  
    1.32  val str = 
    1.33 -"Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = \
    1.34 +"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = \
    1.35  \  (let t_ = Take (F_ v_v = Integral f_ D v_v)                         \
    1.36  \   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)";
    1.37  val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
    1.38 @@ -479,17 +479,17 @@
    1.39  store_met
    1.40      (prep_met Integrate.thy "met_testint" [] e_metID
    1.41  	      (["diff","integration","test"],
    1.42 -	       [("#Given" ,["functionTerm f_", "integrateBy v_v"]),
    1.43 +	       [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.44  		("#Find"  ,["antiDerivative F_"])
    1.45  		],
    1.46  	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [], 
    1.47  		srls = e_rls, 
    1.48  		prls=e_rls,
    1.49  	     crls = Atools_erls, nrls = e_rls},
    1.50 -"Script IntegrationScript (f_::real) (v_v::real) =             \
    1.51 +"Script IntegrationScript (f_f::real) (v_v::real) =             \
    1.52  \  (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \
    1.53  \    (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False)         @@ \
    1.54 -\    (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_::real))"
    1.55 +\    (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_f::real))"
    1.56  ));
    1.57  
    1.58  states:=[];