equal
deleted
inserted
replaced
173 store_pbt |
173 store_pbt |
174 (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID |
174 (prep_pbt thy "pbl_equ_univ_rat" [] e_pblID |
175 (["rational","univariate","equation"], |
175 (["rational","univariate","equation"], |
176 [("#Given" ,["equality e_e","solveFor v_v"]), |
176 [("#Given" ,["equality e_e","solveFor v_v"]), |
177 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), |
177 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), |
178 ("#Find" ,["solutions v'i'"]) |
178 ("#Find" ,["solutions v_v'i'"]) |
179 ], |
179 ], |
180 |
180 |
181 RatEq_prls, SOME "solve (e_e::bool, v_v)", |
181 RatEq_prls, SOME "solve (e_e::bool, v_v)", |
182 [["RatEq","solve_rat_equation"]])); |
182 [["RatEq","solve_rat_equation"]])); |
183 *} |
183 *} |
197 store_met |
197 store_met |
198 (prep_met thy "met_rat_eq" [] e_metID |
198 (prep_met thy "met_rat_eq" [] e_metID |
199 (["RatEq","solve_rat_equation"], |
199 (["RatEq","solve_rat_equation"], |
200 [("#Given" ,["equality e_e","solveFor v_v"]), |
200 [("#Given" ,["equality e_e","solveFor v_v"]), |
201 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), |
201 ("#Where" ,["(e_e::bool) is_ratequation_in (v_v::real)"]), |
202 ("#Find" ,["solutions v'i'"]) |
202 ("#Find" ,["solutions v_v'i'"]) |
203 ], |
203 ], |
204 {rew_ord'="termlessI", |
204 {rew_ord'="termlessI", |
205 rls'=rateq_erls, |
205 rls'=rateq_erls, |
206 srls=e_rls, |
206 srls=e_rls, |
207 prls=RatEq_prls, |
207 prls=RatEq_prls, |