148 ("#Find" ,["solutions v_v'i'"]) |
148 ("#Find" ,["solutions v_v'i'"]) |
149 ], |
149 ], |
150 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", |
150 RootRatEq_prls, SOME "solve (e_e::bool, v_v)", |
151 [["RootRatEq","elim_rootrat_equation"]])); |
151 [["RootRatEq","elim_rootrat_equation"]])); |
152 *} |
152 *} |
153 setup {* KEStore_Elems.store_pbts |
153 setup {* KEStore_Elems.add_pbts |
154 [(prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID |
154 [(prep_pbt thy "pbl_equ_univ_root_sq_rat" [] e_pblID |
155 (["rat","sq","root'","univariate","equation"], |
155 (["rat","sq","root'","univariate","equation"], |
156 [("#Given" ,["equality e_e","solveFor v_v"]), |
156 [("#Given" ,["equality e_e","solveFor v_v"]), |
157 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^ |
157 ("#Where" ,["( (lhs e_e) is_rootRatAddTerm_in (v_v::real) )| " ^ |
158 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), |
158 "( (rhs e_e) is_rootRatAddTerm_in (v_v::real) )"]), |