1.1 --- a/src/Tools/isac/Knowledge/Test.thy	Tue Sep 06 11:47:00 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Test.thy	Wed Sep 07 10:58:12 2022 +0200
     1.3 @@ -566,21 +566,21 @@
     1.4  problem pbl_test : "test" = \<open>Rule_Set.empty\<close>
     1.5  
     1.6  problem pbl_test_equ : "equation/test" =
     1.7 -  \<open>assoc_rls' @{theory} "matches"\<close>
     1.8 +  \<open>get_rls @{context} "matches"\<close>
     1.9    CAS: "solve (e_e::bool, v_v)"
    1.10    Given: "equality e_e" "solveFor v_v"
    1.11    Where: "matches (?a = ?b) e_e"
    1.12    Find: "solutions v_v'i'"
    1.13  
    1.14  problem pbl_test_uni : "univariate/equation/test" =
    1.15 -  \<open>assoc_rls' @{theory} "matches"\<close>
    1.16 +  \<open>get_rls @{context} "matches"\<close>
    1.17    CAS: "solve (e_e::bool, v_v)"
    1.18    Given: "equality e_e" "solveFor v_v"
    1.19    Where: "matches (?a = ?b) e_e"
    1.20    Find: "solutions v_v'i'"
    1.21  
    1.22  problem pbl_test_uni_lin : "LINEAR/univariate/equation/test" =
    1.23 -  \<open>assoc_rls' @{theory} "matches"\<close>
    1.24 +  \<open>get_rls @{context} "matches"\<close>
    1.25    Method_Ref: "Test/solve_linear"
    1.26    CAS: "solve (e_e::bool, v_v)"
    1.27    Given: "equality e_e" "solveFor v_v"
    1.28 @@ -694,7 +694,7 @@
    1.29  section \<open>problems\<close>
    1.30  
    1.31  problem pbl_test_uni_plain2 : "plain_square/univariate/equation/test" =
    1.32 -  \<open>assoc_rls' @{theory} "matches"\<close>
    1.33 +  \<open>get_rls @{context} "matches"\<close>
    1.34    Method_Ref: "Test/solve_plain_square"
    1.35    CAS: "solve (e_e::bool, v_v)"
    1.36    Given: "equality e_e" "solveFor v_v"
    1.37 @@ -778,7 +778,7 @@
    1.38      [e_e])"
    1.39  method met_test_solvelin : "Test/solve_linear" =
    1.40    \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty,
    1.41 -    prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [],
    1.42 +    prls = get_rls @{context} "matches", calc = [], crls = tval_rls, errpats = [],
    1.43      nrls = Test_simplify}\<close>
    1.44    Program: solve_linear.simps
    1.45    Given: "equality e_e" "solveFor v_v"
    1.46 @@ -948,7 +948,7 @@
    1.47  method met_test_eq_plain : "Test/solve_plain_square" =
    1.48    (*solve_plain_square*)
    1.49    \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,calc=[],srls=Rule_Set.empty,
    1.50 -    prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
    1.51 +    prls = get_rls @{context} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,
    1.52      asm_rls=[],asm_thm=[]*)}\<close>
    1.53    Program: solve_plain_square.simps
    1.54    Given: "equality e_e" "solveFor v_v"