equal
deleted
inserted
replaced
199 store_met |
199 store_met |
200 (prep_met thy "met_rateq" [] e_metID |
200 (prep_met thy "met_rateq" [] e_metID |
201 (["RatEq"], |
201 (["RatEq"], |
202 [], |
202 [], |
203 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
203 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
204 crls=RatEq_crls, nrls=norm_Rational |
204 crls=RatEq_crls, nrls = norm_Rational}, "empty_script")); |
205 (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); |
|
206 *} |
205 *} |
207 |
206 |
208 ML {* |
207 ML {* |
209 store_met |
208 store_met |
210 (prep_met thy "met_rat_eq" [] e_metID |
209 (prep_met thy "met_rat_eq" [] e_metID |
216 {rew_ord'="termlessI", |
215 {rew_ord'="termlessI", |
217 rls'=rateq_erls, |
216 rls'=rateq_erls, |
218 srls=e_rls, |
217 srls=e_rls, |
219 prls=RatEq_prls, |
218 prls=RatEq_prls, |
220 calc=[], |
219 calc=[], |
221 crls=RatEq_crls, nrls=norm_Rational}, |
220 crls=RatEq_crls, nrls = norm_Rational}, |
222 "Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^ |
221 "Script Solve_rat_equation (e_e::bool) (v_v::real) = " ^ |
223 "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^ |
222 "(let e_e = ((Repeat(Try (Rewrite_Set RatEq_simplify True))) @@ " ^ |
224 " (Repeat(Try (Rewrite_Set norm_Rational False))) @@ " ^ |
223 " (Repeat(Try (Rewrite_Set norm_Rational False))) @@ " ^ |
225 " (Repeat(Try (Rewrite_Set common_nominator_p False))) @@ " ^ |
224 " (Repeat(Try (Rewrite_Set common_nominator_p False))) @@ " ^ |
226 " (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_e;" ^ |
225 " (Repeat(Try (Rewrite_Set RatEq_eliminate True)))) e_e;" ^ |