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"]),