src/Tools/isac/Knowledge/Integrate.thy
branchisac-update-Isa09-2
changeset 37982 66f3570ba808
parent 37981 b2877b9d455a
child 37983 03bfbc480107
     1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Mon Sep 06 15:09:37 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Mon Sep 06 15:53:18 2010 +0200
     1.3 @@ -367,7 +367,7 @@
     1.4  		srls = e_rls, 
     1.5  		prls=e_rls,
     1.6  	     crls = Atools_erls, nrls = e_rls},
     1.7 -"Script IntegrationScript (f_::real) (v_::real) =                " ^
     1.8 +"Script IntegrationScript (f_::real) (v_v::real) =                " ^
     1.9  "  (let t_ = Take (Integral f_ D v_v)                             " ^
    1.10  "   in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))"
    1.11  ));
    1.12 @@ -382,7 +382,7 @@
    1.13  		srls = e_rls, 
    1.14  		prls=e_rls,
    1.15  		crls = Atools_erls, nrls = e_rls},
    1.16 -"Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = " ^
    1.17 +"Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = " ^
    1.18  "  (let t_ = Take (F_ v_v = Integral f_ D v_v)                            " ^
    1.19  "   in ((Try (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) @@  " ^
    1.20  "       (Rewrite_Set_Inst [(bdv,v_)] integration False)) t_)            "