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