1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Sun Jun 20 12:45:03 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Sun Jun 20 16:26:18 2021 +0200
     1.3 @@ -320,22 +320,21 @@
     1.4    norm_Rational_rls_noadd_fractions = \<open>prep_rls' norm_Rational_rls_noadd_fractions\<close>
     1.5  
     1.6  (** problems **)
     1.7 -setup \<open>KEStore_Elems.add_pbts
     1.8 -  [(Problem.prep_input @{theory} "pbl_fun_integ" [] Problem.id_empty
     1.9 -      (["integrate", "function"],
    1.10 -        [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.11 -          ("#Find"  ,["antiDerivative F_F"])],
    1.12 -        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
    1.13 -        SOME "Integrate (f_f, v_v)", 
    1.14 -        [["diff", "integration"]])),
    1.15 -    (*here "named" is used differently from Differentiation"*)
    1.16 -    (Problem.prep_input @{theory} "pbl_fun_integ_nam" [] Problem.id_empty
    1.17 -      (["named", "integrate", "function"],
    1.18 -        [("#Given" ,["functionTerm f_f", "integrateBy v_v"]),
    1.19 -          ("#Find"  ,["antiDerivativeName F_F"])],
    1.20 -        Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], 
    1.21 -        SOME "Integrate (f_f, v_v)", 
    1.22 -        [["diff", "integration", "named"]]))]\<close>
    1.23 +
    1.24 +problem pbl_fun_integ : "integrate/function" =
    1.25 +  \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
    1.26 +  Method: "diff/integration"
    1.27 +  CAS: "Integrate (f_f, v_v)"
    1.28 +  Given: "functionTerm f_f" "integrateBy v_v"
    1.29 +  Find: "antiDerivative F_F"
    1.30 +
    1.31 +problem pbl_fun_integ_nam : "named/integrate/function" =
    1.32 +  (*here "named" is used differently from Differentiation"*)
    1.33 +  \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
    1.34 +  Method: "diff/integration/named"
    1.35 +  CAS: "Integrate (f_f, v_v)"
    1.36 +  Given: "functionTerm f_f" "integrateBy v_v"
    1.37 +  Find: "antiDerivativeName F_F"
    1.38  
    1.39  (** methods **)
    1.40