38 " (rhs (Subst (v'i', v_v) e_e) || < eps)"]) |
38 " (rhs (Subst (v'i', v_v) e_e) || < eps)"]) |
39 ], |
39 ], |
40 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
40 PolyEq_prls, SOME "solve (e_e::bool, v_v)", |
41 [["Equation","solve_log"]])); |
41 [["Equation","solve_log"]])); |
42 *} |
42 *} |
43 setup {* KEStore_Elems.store_pbts |
43 setup {* KEStore_Elems.add_pbts |
44 [(prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID |
44 [(prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID |
45 (["logarithmic","univariate","equation"], |
45 (["logarithmic","univariate","equation"], |
46 [("#Given",["equality e_e","solveFor v_v"]), |
46 [("#Given",["equality e_e","solveFor v_v"]), |
47 ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]), |
47 ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]), |
48 ("#Find" ,["solutions v_v'i'"]), |
48 ("#Find" ,["solutions v_v'i'"]), |