1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Tue May 28 16:52:30 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed May 29 10:36:16 2019 +0200
     1.3 @@ -355,30 +355,29 @@
     1.4          [["diff","integration","named"]]))]\<close>
     1.5  
     1.6  (** methods **)
     1.7 -(*ok
     1.8 +
     1.9  partial_function (tailrec) integrate :: "real \<Rightarrow> real \<Rightarrow> real"
    1.10    where
    1.11  "integrate f_f v_v =
    1.12    (let t_t = Take (Integral f_f D v_v)
    1.13     in (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False) t_t)"
    1.14 -*)
    1.15  setup \<open>KEStore_Elems.add_mets
    1.16      [Specify.prep_met thy "met_diffint" [] Celem.e_metID
    1.17  	    (["diff","integration"],
    1.18  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find"  ,["antiDerivative F_F"])],
    1.19  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
    1.20  	        crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
    1.21 -	      "Script IntegrationScript (f_f::real) (v_v::real) =                " ^
    1.22 +	      @{thm integrate.simps}
    1.23 +	    (*"Script IntegrationScript (f_f::real) (v_v::real) =                " ^
    1.24            "  (let t_t = Take (Integral f_f D v_v)                             " ^
    1.25 -          "   in (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False) (t_t::real))")]
    1.26 +          "   in (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False) (t_t::real))"*))]
    1.27  \<close>
    1.28 -(*ok
    1.29 +
    1.30  partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
    1.31    where "intergrate_named f_f v_v F_F =
    1.32    (let t_t = Take (F_F v_v = Integral f_f D v_v)
    1.33     in ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'' False)) @@
    1.34         (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False)) t_t)"
    1.35 -*)
    1.36  setup \<open>KEStore_Elems.add_mets
    1.37      [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
    1.38  	    (["diff","integration","named"],
    1.39 @@ -386,10 +385,11 @@
    1.40  	        ("#Find"  ,["antiDerivativeName F_F"])],
    1.41  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
    1.42            crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
    1.43 -        "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
    1.44 +        @{thm intergrate_named.simps}
    1.45 +	    (*"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = " ^
    1.46            "  (let t_t = Take (F_F v_v = Integral f_f D v_v)                            " ^
    1.47            "   in ((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) @@  " ^
    1.48 -          "       (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False)) t_t)            ")]
    1.49 +          "       (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False)) t_t)            "*))]
    1.50  \<close>
    1.51  
    1.52  end
    1.53 \ No newline at end of file