1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Apr 22 11:23:30 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Apr 22 14:36:27 2020 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4  (*----------------------------- problem types --------------------------------*)
     1.5  (* ---------linear----------- *)
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] Spec.e_pblID
     1.8 +  [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] Problem.id_empty
     1.9        (["LINEAR", "univariate", "equation"],
    1.10          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.11            ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
    1.12 @@ -127,7 +127,7 @@
    1.13  
    1.14  (*-------------- methods------------------------------------------------------*)
    1.15  setup \<open>KEStore_Elems.add_mets
    1.16 -    [Specify.prep_met thy "met_eqlin" [] Spec.e_metID
    1.17 +    [Specify.prep_met thy "met_eqlin" [] Method.id_empty
    1.18        (["LinEq"], [],
    1.19          {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.20            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.21 @@ -151,7 +151,7 @@
    1.22    in
    1.23      Or_to_List e_e)"
    1.24  setup \<open>KEStore_Elems.add_mets
    1.25 -    [Specify.prep_met thy "met_eq_lin" [] Spec.e_metID
    1.26 +    [Specify.prep_met thy "met_eq_lin" [] Method.id_empty
    1.27        (["LinEq","solve_lineq_equation"],
    1.28          [("#Given", ["equality e_e", "solveFor v_v"]),
    1.29            ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),