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"