diff -r ae5f26c14181 -r 2406d378cede src/Tools/isac/Knowledge/PolyEq.thy
--- a/src/Tools/isac/Knowledge/PolyEq.thy	Wed Jun 01 13:39:41 2022 +0200
+++ b/src/Tools/isac/Knowledge/PolyEq.thy	Wed Jun 01 14:17:23 2022 +0200
@@ -639,7 +639,7 @@
 (*--- d0 ---*)
 problem pbl_equ_univ_poly_deg0 : "degree_0/polynomial/univariate/equation" =
   \<open>PolyEq_prls\<close>
-  Method: "PolyEq/solve_d0_polyeq_equation"
+  Method_Ref: "PolyEq/solve_d0_polyeq_equation"
   CAS: "solve (e_e::bool, v_v)"
   Given: "equality e_e" "solveFor v_v"
   Where:
@@ -651,7 +651,7 @@
 (*--- d1 ---*)
 problem pbl_equ_univ_poly_deg1 : "degree_1/polynomial/univariate/equation" =
   \<open>PolyEq_prls\<close>
-  Method: "PolyEq/solve_d1_polyeq_equation"
+  Method_Ref: "PolyEq/solve_d1_polyeq_equation"
   CAS: "solve (e_e::bool, v_v)"
   Given: "equality e_e" "solveFor v_v"
   Where:
@@ -663,7 +663,7 @@
 (*--- d2 ---*)
 problem pbl_equ_univ_poly_deg2 : "degree_2/polynomial/univariate/equation" =
   \<open>PolyEq_prls\<close>
-  Method: "PolyEq/solve_d2_polyeq_equation"
+  Method_Ref: "PolyEq/solve_d2_polyeq_equation"
   CAS: "solve (e_e::bool, v_v)"
   Given: "equality e_e" "solveFor v_v"
   Where:
@@ -674,7 +674,7 @@
 
 problem pbl_equ_univ_poly_deg2_sqonly : "sq_only/degree_2/polynomial/univariate/equation" =
   \<open>PolyEq_prls\<close>
-  Method: "PolyEq/solve_d2_polyeq_sqonly_equation"
+  Method_Ref: "PolyEq/solve_d2_polyeq_sqonly_equation"
   CAS: "solve (e_e::bool, v_v)"
   Given: "equality e_e" "solveFor v_v"
   Where:
@@ -694,7 +694,7 @@
 
 problem pbl_equ_univ_poly_deg2_bdvonly : "bdv_only/degree_2/polynomial/univariate/equation" =
   \<open>PolyEq_prls\<close>
-  Method: "PolyEq/solve_d2_polyeq_bdvonly_equation"
+  Method_Ref: "PolyEq/solve_d2_polyeq_bdvonly_equation"
   CAS: "solve (e_e::bool, v_v)"
   Given: "equality e_e" "solveFor v_v"
   Where:
@@ -708,7 +708,7 @@
 
 problem pbl_equ_univ_poly_deg2_pq : "pqFormula/degree_2/polynomial/univariate/equation" =
   \<open>PolyEq_prls\<close>
-  Method: "PolyEq/solve_d2_polyeq_pq_equation"
+  Method_Ref: "PolyEq/solve_d2_polyeq_pq_equation"
   CAS: "solve (e_e::bool, v_v)"
   Given: "equality e_e" "solveFor v_v"
   Where:
@@ -718,7 +718,7 @@
 
 problem pbl_equ_univ_poly_deg2_abc : "abcFormula/degree_2/polynomial/univariate/equation" =
   \<open>PolyEq_prls\<close>
-  Method: "PolyEq/solve_d2_polyeq_abc_equation"
+  Method_Ref: "PolyEq/solve_d2_polyeq_abc_equation"
   CAS: "solve (e_e::bool, v_v)"
   Given: "equality e_e" "solveFor v_v"
   Where:
@@ -729,7 +729,7 @@
 (*--- d3 ---*)
 problem pbl_equ_univ_poly_deg3 : "degree_3/polynomial/univariate/equation" =
   \<open>PolyEq_prls\<close>
-  Method: "PolyEq/solve_d3_polyeq_equation"
+  Method_Ref: "PolyEq/solve_d3_polyeq_equation"
   CAS: "solve (e_e::bool, v_v)"
   Given: "equality e_e" "solveFor v_v"
   Where:
@@ -753,7 +753,7 @@
 (*--- normalise ---*)
 problem pbl_equ_univ_poly_norm : "normalise/polynomial/univariate/equation" =
   \<open>PolyEq_prls\<close>
-  Method: "PolyEq/normalise_poly"
+  Method_Ref: "PolyEq/normalise_poly"
   CAS: "solve (e_e::bool, v_v)"
   Given: "equality e_e" "solveFor v_v"
   Where:
@@ -774,7 +774,7 @@
 (*--- d2 ---*)
 problem pbl_equ_univ_expand_deg2 : "degree_2/expanded/univariate/equation" =
   \<open>PolyEq_prls\<close>
-  Method: "PolyEq/complete_square"
+  Method_Ref: "PolyEq/complete_square"
   CAS: "solve (e_e::bool, v_v)"
   Given: "equality e_e" "solveFor v_v"
   Where: "((lhs e_e) has_degree_in v_v) = 2"