1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Sat Jun 12 18:33:15 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Tue Jun 15 22:24:20 2021 +0200
     1.3 @@ -346,14 +346,13 @@
     1.4      t_t = Take (Integral f_f D v_v)
     1.5    in
     1.6      (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)"
     1.7 -setup \<open>KEStore_Elems.add_mets
     1.8 -    [MethodC.prep_input @{theory} "met_diffint" [] MethodC.id_empty
     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_Set.empty, prls=Rule_Set.empty,
    1.12 -	        crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
    1.13 -	      @{thm integrate.simps})]
    1.14 -\<close>
    1.15 +
    1.16 +method met_diffint : "diff/integration" =
    1.17 +  \<open>{rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    1.18 +	  crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
    1.19 +  Program: integrate.simps
    1.20 +  Given: "functionTerm f_f" "integrateBy v_v"
    1.21 +  Find: "antiDerivative F_F"
    1.22  
    1.23  partial_function (tailrec) intergrate_named :: "real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool"
    1.24    where
    1.25 @@ -364,15 +363,15 @@
    1.26      (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) #>
    1.27      (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'')
    1.28      ) t_t)"
    1.29 -setup \<open>KEStore_Elems.add_mets
    1.30 -    [MethodC.prep_input @{theory} "met_diffint_named" [] MethodC.id_empty
    1.31 -	    (["diff", "integration", "named"],
    1.32 -	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.33 -	        ("#Find"  ,["antiDerivativeName F_F"])],
    1.34 -	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    1.35 -          crls = Atools_erls, errpats = [], nrls = Rule_Set.empty},
    1.36 -        @{thm intergrate_named.simps})]
    1.37 -\<close> ML \<open>
    1.38 +
    1.39 +method met_diffint_named : "diff/integration/named" =
    1.40 +  \<open>{rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
    1.41 +    crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}\<close>
    1.42 +  Program: intergrate_named.simps
    1.43 +  Given: "functionTerm f_f" "integrateBy v_v"
    1.44 +  Find: "antiDerivativeName F_F"
    1.45 +
    1.46 +ML \<open>
    1.47  \<close> ML \<open>
    1.48  \<close>
    1.49