1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Fri Feb 15 16:52:05 2019 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Tue Feb 19 19:35:12 2019 +0100
     1.3 @@ -355,6 +355,11 @@
     1.4          [["diff","integration","named"]]))]\<close>
     1.5  
     1.6  (** methods **)
     1.7 +partial_function (tailrec) integrate :: "real \<Rightarrow> real \<Rightarrow> real"
     1.8 +  where
     1.9 +"integrate f_f v_v =
    1.10 +  (let t_t = Take (Integral f_f D v_v)
    1.11 +   in (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False) t_t)"
    1.12  setup \<open>KEStore_Elems.add_mets
    1.13      [Specify.prep_met thy "met_diffint" [] Celem.e_metID
    1.14  	    (["diff","integration"],
    1.15 @@ -365,6 +370,11 @@
    1.16            "  (let t_t = Take (Integral f_f D v_v)                             " ^
    1.17            "   in (Rewrite_Set_Inst [(''bdv'',v_v)] ''integration'' False) (t_t::real))")]
    1.18  \<close>
    1.19 +partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
    1.20 +  where "intergrate_named f_f v_v F_F =
    1.21 +  (let t_t = Take (F_F v_v = Integral f_f D v_v)
    1.22 +   in ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'' False)) @@
    1.23 +       (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False)) t_t)"
    1.24  setup \<open>KEStore_Elems.add_mets
    1.25      [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
    1.26  	    (["diff","integration","named"],