1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy Sun Feb 02 02:45:11 2014 +0100
1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy Sun Feb 02 03:09:40 2014 +0100
1.3 @@ -132,39 +132,6 @@
1.4 ("#Find" ,["solutions v_v'i'"])],
1.5 LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))] *}
1.6
1.7 -ML {*
1.8 -(*-------------- methods------------------------------------------------------*)
1.9 -store_met
1.10 - (prep_met thy "met_eqlin" [] e_metID
1.11 - (["LinEq"],
1.12 - [],
1.13 - {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
1.14 - crls=LinEq_crls, errpats = [], nrls = norm_Poly}, "empty_script"));
1.15 -
1.16 -(* ansprechen mit ["LinEq","solve_univar_equation"] *)
1.17 -store_met
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)",
1.22 - "((lhs e_e) has_degree_in v_v) = 1"]),
1.23 - ("#Find", ["solutions v_v'i'"])
1.24 - ],
1.25 - {rew_ord'="termlessI", rls'=LinEq_erls, srls=e_rls, prls=LinEq_prls,
1.26 - calc=[], crls=LinEq_crls, errpats = [], nrls = norm_Poly},
1.27 - "Script Solve_lineq_equation (e_e::bool) (v_v::real) = " ^
1.28 - "(let e_e =((Try (Rewrite all_left False)) @@ " ^
1.29 - " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
1.30 - " (Try (Rewrite_Set expand_binoms False)) @@ " ^
1.31 - " (Try (Repeat (Rewrite_Set_Inst [(bdv, v_v::real)] " ^
1.32 - " make_ratpoly_in False))) @@ " ^
1.33 - " (Try (Repeat (Rewrite_Set LinPoly_simplify False))))e_e;" ^
1.34 - " e_e = ((Try (Rewrite_Set_Inst [(bdv, v_v::real)] " ^
1.35 - " LinEq_simplify True)) @@ " ^
1.36 - " (Repeat(Try (Rewrite_Set LinPoly_simplify False)))) e_e " ^
1.37 - " in ((Or_to_List e_e)::bool list))"
1.38 - ));
1.39 -*}
1.40 (*-------------- methods------------------------------------------------------*)
1.41 setup {* KEStore_Elems.add_mets
1.42 [prep_met thy "met_eqlin" [] e_metID