1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Wed Jun 01 13:39:41 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Wed Jun 01 14:17:23 2022 +0200
     1.3 @@ -639,7 +639,7 @@
     1.4  (*--- d0 ---*)
     1.5  problem pbl_equ_univ_poly_deg0 : "degree_0/polynomial/univariate/equation" =
     1.6    \<open>PolyEq_prls\<close>
     1.7 -  Method: "PolyEq/solve_d0_polyeq_equation"
     1.8 +  Method_Ref: "PolyEq/solve_d0_polyeq_equation"
     1.9    CAS: "solve (e_e::bool, v_v)"
    1.10    Given: "equality e_e" "solveFor v_v"
    1.11    Where:
    1.12 @@ -651,7 +651,7 @@
    1.13  (*--- d1 ---*)
    1.14  problem pbl_equ_univ_poly_deg1 : "degree_1/polynomial/univariate/equation" =
    1.15    \<open>PolyEq_prls\<close>
    1.16 -  Method: "PolyEq/solve_d1_polyeq_equation"
    1.17 +  Method_Ref: "PolyEq/solve_d1_polyeq_equation"
    1.18    CAS: "solve (e_e::bool, v_v)"
    1.19    Given: "equality e_e" "solveFor v_v"
    1.20    Where:
    1.21 @@ -663,7 +663,7 @@
    1.22  (*--- d2 ---*)
    1.23  problem pbl_equ_univ_poly_deg2 : "degree_2/polynomial/univariate/equation" =
    1.24    \<open>PolyEq_prls\<close>
    1.25 -  Method: "PolyEq/solve_d2_polyeq_equation"
    1.26 +  Method_Ref: "PolyEq/solve_d2_polyeq_equation"
    1.27    CAS: "solve (e_e::bool, v_v)"
    1.28    Given: "equality e_e" "solveFor v_v"
    1.29    Where:
    1.30 @@ -674,7 +674,7 @@
    1.31  
    1.32  problem pbl_equ_univ_poly_deg2_sqonly : "sq_only/degree_2/polynomial/univariate/equation" =
    1.33    \<open>PolyEq_prls\<close>
    1.34 -  Method: "PolyEq/solve_d2_polyeq_sqonly_equation"
    1.35 +  Method_Ref: "PolyEq/solve_d2_polyeq_sqonly_equation"
    1.36    CAS: "solve (e_e::bool, v_v)"
    1.37    Given: "equality e_e" "solveFor v_v"
    1.38    Where:
    1.39 @@ -694,7 +694,7 @@
    1.40  
    1.41  problem pbl_equ_univ_poly_deg2_bdvonly : "bdv_only/degree_2/polynomial/univariate/equation" =
    1.42    \<open>PolyEq_prls\<close>
    1.43 -  Method: "PolyEq/solve_d2_polyeq_bdvonly_equation"
    1.44 +  Method_Ref: "PolyEq/solve_d2_polyeq_bdvonly_equation"
    1.45    CAS: "solve (e_e::bool, v_v)"
    1.46    Given: "equality e_e" "solveFor v_v"
    1.47    Where:
    1.48 @@ -708,7 +708,7 @@
    1.49  
    1.50  problem pbl_equ_univ_poly_deg2_pq : "pqFormula/degree_2/polynomial/univariate/equation" =
    1.51    \<open>PolyEq_prls\<close>
    1.52 -  Method: "PolyEq/solve_d2_polyeq_pq_equation"
    1.53 +  Method_Ref: "PolyEq/solve_d2_polyeq_pq_equation"
    1.54    CAS: "solve (e_e::bool, v_v)"
    1.55    Given: "equality e_e" "solveFor v_v"
    1.56    Where:
    1.57 @@ -718,7 +718,7 @@
    1.58  
    1.59  problem pbl_equ_univ_poly_deg2_abc : "abcFormula/degree_2/polynomial/univariate/equation" =
    1.60    \<open>PolyEq_prls\<close>
    1.61 -  Method: "PolyEq/solve_d2_polyeq_abc_equation"
    1.62 +  Method_Ref: "PolyEq/solve_d2_polyeq_abc_equation"
    1.63    CAS: "solve (e_e::bool, v_v)"
    1.64    Given: "equality e_e" "solveFor v_v"
    1.65    Where:
    1.66 @@ -729,7 +729,7 @@
    1.67  (*--- d3 ---*)
    1.68  problem pbl_equ_univ_poly_deg3 : "degree_3/polynomial/univariate/equation" =
    1.69    \<open>PolyEq_prls\<close>
    1.70 -  Method: "PolyEq/solve_d3_polyeq_equation"
    1.71 +  Method_Ref: "PolyEq/solve_d3_polyeq_equation"
    1.72    CAS: "solve (e_e::bool, v_v)"
    1.73    Given: "equality e_e" "solveFor v_v"
    1.74    Where:
    1.75 @@ -753,7 +753,7 @@
    1.76  (*--- normalise ---*)
    1.77  problem pbl_equ_univ_poly_norm : "normalise/polynomial/univariate/equation" =
    1.78    \<open>PolyEq_prls\<close>
    1.79 -  Method: "PolyEq/normalise_poly"
    1.80 +  Method_Ref: "PolyEq/normalise_poly"
    1.81    CAS: "solve (e_e::bool, v_v)"
    1.82    Given: "equality e_e" "solveFor v_v"
    1.83    Where:
    1.84 @@ -774,7 +774,7 @@
    1.85  (*--- d2 ---*)
    1.86  problem pbl_equ_univ_expand_deg2 : "degree_2/expanded/univariate/equation" =
    1.87    \<open>PolyEq_prls\<close>
    1.88 -  Method: "PolyEq/complete_square"
    1.89 +  Method_Ref: "PolyEq/complete_square"
    1.90    CAS: "solve (e_e::bool, v_v)"
    1.91    Given: "equality e_e" "solveFor v_v"
    1.92    Where: "((lhs e_e) has_degree_in v_v) = 2"