1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -127,7 +127,7 @@
     1.4  
     1.5  (*-------------- methods------------------------------------------------------*)
     1.6  setup \<open>KEStore_Elems.add_mets
     1.7 -    [Method.prep_input thy "met_eqlin" [] Method.id_empty
     1.8 +    [MethodC.prep_input thy "met_eqlin" [] MethodC.id_empty
     1.9        (["LinEq"], [],
    1.10          {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.11            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.12 @@ -151,7 +151,7 @@
    1.13    in
    1.14      Or_to_List e_e)"
    1.15  setup \<open>KEStore_Elems.add_mets
    1.16 -    [Method.prep_input thy "met_eq_lin" [] Method.id_empty
    1.17 +    [MethodC.prep_input thy "met_eq_lin" [] MethodC.id_empty
    1.18        (["LinEq", "solve_lineq_equation"],
    1.19          [("#Given", ["equality e_e", "solveFor v_v"]),
    1.20            ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),
    1.21 @@ -160,7 +160,7 @@
    1.22            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.23          @{thm solve_linear_equation.simps})]
    1.24  \<close>
    1.25 -ML \<open>Method.from_store' @{theory} ["LinEq", "solve_lineq_equation"];\<close>
    1.26 +ML \<open>MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];\<close>
    1.27  
    1.28  end
    1.29