1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Dec 14 14:20:25 2016 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Sun Dec 18 16:27:41 2016 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4  (*----------------------------- problem types --------------------------------*)
     1.5  (* ---------linear----------- *)
     1.6  setup {* KEStore_Elems.add_pbts
     1.7 -  [(prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
     1.8 +  [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
     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 @@ -134,13 +134,13 @@
    1.13  
    1.14  (*-------------- methods------------------------------------------------------*)
    1.15  setup {* KEStore_Elems.add_mets
    1.16 -  [prep_met thy "met_eqlin" [] e_metID
    1.17 +  [Specify.prep_met thy "met_eqlin" [] e_metID
    1.18        (["LinEq"], [],
    1.19          {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = e_rls, prls = e_rls,
    1.20            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.21          "empty_script"),
    1.22      (* ansprechen mit ["LinEq","solve_univar_equation"] *)
    1.23 -    prep_met thy "met_eq_lin" [] e_metID
    1.24 +    Specify.prep_met thy "met_eq_lin" [] e_metID
    1.25        (["LinEq","solve_lineq_equation"],
    1.26          [("#Given", ["equality e_e", "solveFor v_v"]),
    1.27            ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),
    1.28 @@ -159,7 +159,7 @@
    1.29            "            (Repeat(Try (Rewrite_Set LinPoly_simplify     False)))) e_e " ^
    1.30            " in ((Or_to_List e_e)::bool list))")]
    1.31  *}
    1.32 -ML {* get_met' @{theory} ["LinEq","solve_lineq_equation"]; *}
    1.33 +ML {* Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"]; *}
    1.34  
    1.35  end
    1.36