src/Tools/isac/Knowledge/Integrate.thy
changeset 60449 2406d378cede
parent 60368 d2f2386f3f06
child 60504 8cc1415b3530
     1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Wed Jun 01 13:39:41 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Wed Jun 01 14:17:23 2022 +0200
     1.3 @@ -258,7 +258,7 @@
     1.4  
     1.5  problem pbl_fun_integ : "integrate/function" =
     1.6    \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
     1.7 -  Method: "diff/integration"
     1.8 +  Method_Ref: "diff/integration"
     1.9    CAS: "Integrate (f_f, v_v)"
    1.10    Given: "functionTerm f_f" "integrateBy v_v"
    1.11    Find: "antiDerivative F_F"
    1.12 @@ -266,7 +266,7 @@
    1.13  problem pbl_fun_integ_nam : "named/integrate/function" =
    1.14    (*here "named" is used differently from Differentiation"*)
    1.15    \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)]\<close>
    1.16 -  Method: "diff/integration/named"
    1.17 +  Method_Ref: "diff/integration/named"
    1.18    CAS: "Integrate (f_f, v_v)"
    1.19    Given: "functionTerm f_f" "integrateBy v_v"
    1.20    Find: "antiDerivativeName F_F"