1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Jun 01 13:39:41 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Wed Jun 01 14:17:23 2022 +0200
     1.3 @@ -340,7 +340,7 @@
     1.4       \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
     1.5       \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
     1.6       \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close>
     1.7 -  Method: "simplification/for_polynomials/with_minus"
     1.8 +  Method_Ref: "simplification/for_polynomials/with_minus"
     1.9    CAS: "Vereinfache t_t"
    1.10    Given: "Term t_t"
    1.11    Where:
    1.12 @@ -363,7 +363,7 @@
    1.13       \<^rule_thm>\<open>or_false\<close>, (*"(?a | False) = ?a"*)
    1.14       \<^rule_thm>\<open>not_true\<close>, (*"(~ True) = False"*)
    1.15       \<^rule_thm>\<open>not_false\<close> (*"(~ False) = True"*)]\<close>
    1.16 -  Method: "simplification/for_polynomials/with_parentheses"
    1.17 +  Method_Ref: "simplification/for_polynomials/with_parentheses"
    1.18    CAS: "Vereinfache t_t"
    1.19    Given: "Term t_t"
    1.20    Where:
    1.21 @@ -377,7 +377,7 @@
    1.22  problem pbl_vereinf_poly_klammer_mal : "binom_klammer/polynom/vereinfachen" =
    1.23    \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
    1.24      \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
    1.25 -  Method: "simplification/for_polynomials/with_parentheses_mult"
    1.26 +  Method_Ref: "simplification/for_polynomials/with_parentheses_mult"
    1.27    CAS: "Vereinfache t_t"
    1.28    Given: "Term t_t"
    1.29    Where: "t_t is_polyexp"
    1.30 @@ -388,7 +388,7 @@
    1.31  problem pbl_probe_poly : "polynom/probe" =
    1.32    \<open>Rule_Set.append_rules "prls_pbl_probe_poly" Rule_Set.empty [(*for preds in where_*)
    1.33      \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
    1.34 -  Method: "probe/fuer_polynom"
    1.35 +  Method_Ref: "probe/fuer_polynom"
    1.36    CAS: "Probe e_e w_w"
    1.37    Given: "Pruefe e_e" "mitWert w_w"
    1.38    Where: "e_e is_polyexp"
    1.39 @@ -397,7 +397,7 @@
    1.40  problem pbl_probe_bruch : "bruch/probe" =
    1.41    \<open>Rule_Set.append_rules "prls_pbl_probe_bruch" Rule_Set.empty [(*for preds in where_*)
    1.42      \<^rule_eval>\<open>is_ratpolyexp\<close> (eval_is_ratpolyexp "")]\<close>
    1.43 -  Method: "probe/fuer_bruch"
    1.44 +  Method_Ref: "probe/fuer_bruch"
    1.45    CAS: "Probe e_e w_w"
    1.46    Given: "Pruefe e_e" "mitWert w_w"
    1.47    Where: "e_e is_ratpolyexp"