src/Tools/isac/Knowledge/LinEq.thy
changeset 59473 28b67cae58c3
parent 59472 3e904f8ec16c
child 59489 cfcbcac0bae8
     1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Nov 21 12:32:54 2018 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Nov 28 11:46:00 2018 +0100
     1.3 @@ -133,13 +133,15 @@
     1.4  
     1.5  (*-------------- methods------------------------------------------------------*)
     1.6  setup \<open>KEStore_Elems.add_mets
     1.7 -  [Specify.prep_met thy "met_eqlin" [] Celem.e_metID
     1.8 +    [Specify.prep_met thy "met_eqlin" [] Celem.e_metID
     1.9        (["LinEq"], [],
    1.10          {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
    1.11            crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.12 -        "empty_script"),
    1.13 +        "empty_script")]
    1.14 +\<close>
    1.15      (* ansprechen mit ["LinEq","solve_univar_equation"] *)
    1.16 -    Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
    1.17 +setup \<open>KEStore_Elems.add_mets
    1.18 +    [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
    1.19        (["LinEq","solve_lineq_equation"],
    1.20          [("#Given", ["equality e_e", "solveFor v_v"]),
    1.21            ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),