138 ("#Find" ,["solutions v_v'i'"]) |
138 ("#Find" ,["solutions v_v'i'"]) |
139 ], |
139 ], |
140 LinEq_prls, SOME "solve (e_e::bool, v_v)", |
140 LinEq_prls, SOME "solve (e_e::bool, v_v)", |
141 [["LinEq","solve_lineq_equation"]])); |
141 [["LinEq","solve_lineq_equation"]])); |
142 *} |
142 *} |
143 setup {* KEStore_Elems.store_pbts |
143 setup {* KEStore_Elems.add_pbts |
144 [(prep_pbt thy "pbl_equ_univ_lin" [] e_pblID |
144 [(prep_pbt thy "pbl_equ_univ_lin" [] e_pblID |
145 (["LINEAR", "univariate", "equation"], |
145 (["LINEAR", "univariate", "equation"], |
146 [("#Given" ,["equality e_e", "solveFor v_v"]), |
146 [("#Given" ,["equality e_e", "solveFor v_v"]), |
147 ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*) |
147 ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*) |
148 "Not( (lhs e_e) is_polyrat_in v_v)", |
148 "Not( (lhs e_e) is_polyrat_in v_v)", |