1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Sat Jun 12 18:33:15 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Jun 15 22:24:20 2021 +0200
     1.3 @@ -121,13 +121,9 @@
     1.4          LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))]\<close>
     1.5  
     1.6  (*-------------- methods------------------------------------------------------*)
     1.7 -setup \<open>KEStore_Elems.add_mets
     1.8 -    [MethodC.prep_input @{theory} "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 -        @{thm refl})]
    1.13 -\<close>
    1.14 +method met_eqlin : "LinEq" =
    1.15 +  \<open>{rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
    1.16 +    crls = LinEq_crls, errpats = [], nrls = norm_Poly}\<close>
    1.17      (* ansprechen mit ["LinEq", "solve_univar_equation"] *)
    1.18  
    1.19  partial_function (tailrec) solve_linear_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list"
    1.20 @@ -145,16 +141,15 @@
    1.21        (Repeat (Try (Rewrite_Set ''LinPoly_simplify''))) ) e_e
    1.22    in
    1.23      Or_to_List e_e)"
    1.24 -setup \<open>KEStore_Elems.add_mets
    1.25 -    [MethodC.prep_input @{theory} "met_eq_lin" [] MethodC.id_empty
    1.26 -      (["LinEq", "solve_lineq_equation"],
    1.27 -        [("#Given", ["equality e_e", "solveFor v_v"]),
    1.28 -          ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),
    1.29 -          ("#Find",  ["solutions v_v'i'"])],
    1.30 -        {rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule_Set.empty, prls = LinEq_prls, calc = [],
    1.31 -          crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.32 -        @{thm solve_linear_equation.simps})]
    1.33 -\<close>
    1.34 +
    1.35 +method met_eq_lin : "LinEq/solve_lineq_equation" =
    1.36 +  \<open>{rew_ord' = "termlessI", rls' = LinEq_erls, srls = Rule_Set.empty, prls = LinEq_prls, calc = [],
    1.37 +    crls = LinEq_crls, errpats = [], nrls = norm_Poly}\<close>
    1.38 +  Program: solve_linear_equation.simps
    1.39 +  Given: "equality e_e" "solveFor v_v"
    1.40 +  Where: "Not ((lhs e_e) is_polyrat_in v_v)" "((lhs e_e)  has_degree_in v_v) = 1"
    1.41 +  Find: "solutions v_v'i'"
    1.42 +
    1.43  ML \<open>
    1.44    MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];
    1.45  \<close> ML \<open>