1.1 --- a/test/Tools/isac/Knowledge/integrate.sml Wed Oct 06 14:35:43 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed Oct 06 14:52:12 2010 +0200
1.3 @@ -341,10 +341,9 @@
1.4 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
1.5 | _ => error "integrate.sml: Integrate.antiDerivative ???";
1.6
1.7 -(*=== inhibit exn ?=============================================================
1.8 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
1.9 Where =[],
1.10 - Find =["antiDerivativeName F_"],
1.11 + Find =["antiDerivativeName F_F"],
1.12 With =[],
1.13 Relate=[]}:string ppc;
1.14 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
1.15 @@ -357,7 +356,7 @@
1.16 "----- compare 'Find's from problem, script, formalization -------";
1.17 val {ppc,...} = get_pbt ["named","integrate","function"];
1.18 val ("#Find", (Const ("Integrate.antiDerivativeName", _),
1.19 - F1_ as Free ("F_", F1_type))) = last_elem ppc;
1.20 + F1_ as Free ("F_F", F1_type))) = last_elem ppc;
1.21 val {scr = Script sc,... } = get_met ["diff","integration","named"];
1.22 val [_,_, F2_] = formal_args sc;
1.23 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
1.24 @@ -379,15 +378,15 @@
1.25 "----------- check Scripts ------------------------------";
1.26 val str =
1.27 "Script IntegrationScript (f_f::real) (v_v::real) = \
1.28 -\ (let t_ = Take (Integral f_ D v_v) \
1.29 -\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))";
1.30 +\ (let t_t = Take (Integral f_f D v_v) \
1.31 +\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))";
1.32 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.33 atomty sc;
1.34
1.35 val str =
1.36 -"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = \
1.37 -\ (let t_ = Take (F_ v_v = Integral f_ D v_v) \
1.38 -\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)";
1.39 +"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
1.40 +\ (let t_t = Take (F_F v_v = Integral f_f D v_v) \
1.41 +\ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_t)";
1.42 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
1.43 atomty sc;
1.44 show_mets();
1.45 @@ -418,6 +417,7 @@
1.46 else error "integrate.sml: method [diff,integration]";
1.47
1.48
1.49 +(*=== inhibit exn ?=============================================================
1.50 "----------- me method [diff,integration,named] ---------";
1.51 "----------- me method [diff,integration,named] ---------";
1.52 "----------- me method [diff,integration,named] ---------";
1.53 @@ -496,7 +496,7 @@
1.54 (prep_met thy "met_testint" [] e_metID
1.55 (["diff","integration","test"],
1.56 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
1.57 - ("#Find" ,["antiDerivative F_"])
1.58 + ("#Find" ,["antiDerivative F_F"])
1.59 ],
1.60 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
1.61 srls = e_rls,