1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Sep 26 17:47:10 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Tue Oct 01 10:47:25 2019 +0200
     1.3 @@ -351,9 +351,11 @@
     1.4  
     1.5  partial_function (tailrec) integrate :: "real \<Rightarrow> real \<Rightarrow> real"
     1.6    where
     1.7 -"integrate f_f v_v =
     1.8 -  (let t_t = Take (Integral f_f D v_v)
     1.9 -   in (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False) t_t)"
    1.10 +"integrate f_f v_v = (
    1.11 +  let
    1.12 +    t_t = Take (Integral f_f D v_v)
    1.13 +  in
    1.14 +    (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
    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 @@ -364,10 +366,14 @@
    1.19  \<close>
    1.20  
    1.21  partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
    1.22 -  where "intergrate_named f_f v_v F_F =
    1.23 -  (let t_t = Take (F_F v_v = Integral f_f D v_v)
    1.24 -   in ((Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'' False)) @@
    1.25 -       (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'' False)) t_t)"
    1.26 +  where
    1.27 +"intergrate_named f_f v_v F_F =(
    1.28 +  let
    1.29 +    t_t = Take (F_F v_v = Integral f_f D v_v)
    1.30 +  in (
    1.31 +    (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) @@
    1.32 +    (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
    1.33 +    ) t_t)"
    1.34  setup \<open>KEStore_Elems.add_mets
    1.35      [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
    1.36  	    (["diff","integration","named"],