1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Fri Jan 31 17:50:50 2014 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Sat Feb 01 16:44:45 2014 +0100
     1.3 @@ -164,9 +164,35 @@
     1.4      "            (Repeat(Try (Rewrite_Set LinPoly_simplify     False)))) e_e " ^
     1.5      " in ((Or_to_List e_e)::bool list))"
     1.6   ));
     1.7 -get_met ["LinEq","solve_lineq_equation"];
     1.8 -
     1.9  *}
    1.10 +(*-------------- methods------------------------------------------------------*)
    1.11 +setup {* KEStore_Elems.add_mets
    1.12 +  [prep_met thy "met_eqlin" [] e_metID
    1.13 +      (["LinEq"], [],
    1.14 +        {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = e_rls, prls = e_rls,
    1.15 +          crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.16 +        "empty_script"),
    1.17 +    (* ansprechen mit ["LinEq","solve_univar_equation"] *)
    1.18 +    prep_met thy "met_eq_lin" [] 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"]),
    1.22 +          ("#Find",  ["solutions v_v'i'"])],
    1.23 +        {rew_ord' = "termlessI", rls' = LinEq_erls, srls = e_rls, prls = LinEq_prls, calc = [],
    1.24 +          crls = LinEq_crls, errpats = [], nrls = norm_Poly},
    1.25 +        "Script Solve_lineq_equation (e_e::bool) (v_v::real) =                 " ^
    1.26 +          "(let e_e =((Try         (Rewrite      all_left           False)) @@   " ^ 
    1.27 +          "           (Try (Repeat (Rewrite     makex1_x            False))) @@  " ^ 
    1.28 +          "           (Try         (Rewrite_Set expand_binoms       False)) @@   " ^ 
    1.29 +          "           (Try (Repeat (Rewrite_Set_Inst [(bdv, v_v::real)]          " ^
    1.30 +          "                                 make_ratpoly_in    False)))    @@    " ^
    1.31 +          "           (Try (Repeat (Rewrite_Set LinPoly_simplify      False))))e_e;" ^
    1.32 +          "     e_e = ((Try (Rewrite_Set_Inst [(bdv, v_v::real)]                  " ^
    1.33 +          "                                     LinEq_simplify True)) @@  " ^
    1.34 +          "            (Repeat(Try (Rewrite_Set LinPoly_simplify     False)))) e_e " ^
    1.35 +          " in ((Or_to_List e_e)::bool list))")]
    1.36 +*}
    1.37 +ML {* get_met ["LinEq","solve_lineq_equation"]; *}
    1.38  
    1.39  end
    1.40