1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Nov 21 12:32:54 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Nov 28 11:46:00 2018 +0100
     1.3 @@ -356,15 +356,17 @@
     1.4  
     1.5  (** methods **)
     1.6  setup \<open>KEStore_Elems.add_mets
     1.7 -  [Specify.prep_met thy "met_diffint" [] Celem.e_metID
     1.8 +    [Specify.prep_met thy "met_diffint" [] Celem.e_metID
     1.9  	    (["diff","integration"],
    1.10  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find"  ,["antiDerivative F_F"])],
    1.11  	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls,
    1.12  	        crls = Atools_erls, errpats = [], nrls = Rule.e_rls},
    1.13  	      "Script IntegrationScript (f_f::real) (v_v::real) =                " ^
    1.14            "  (let t_t = Take (Integral f_f D v_v)                             " ^
    1.15 -          "   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"),
    1.16 -    Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
    1.17 +          "   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))")]
    1.18 +\<close>
    1.19 +setup \<open>KEStore_Elems.add_mets
    1.20 +    [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID
    1.21  	    (["diff","integration","named"],
    1.22  	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.23  	        ("#Find"  ,["antiDerivativeName F_F"])],