diff -r 24609758d219 -r 028442673981 src/Tools/isac/Knowledge/LogExp.thy --- a/src/Tools/isac/Knowledge/LogExp.thy Wed Sep 08 16:45:27 2010 +0200 +++ b/src/Tools/isac/Knowledge/LogExp.thy Wed Sep 08 16:47:22 2010 +0200 @@ -32,10 +32,10 @@ (prep_pbt thy "pbl_test_equ_univ_log" [] e_pblID (["logarithmic","univariate","equation"], [("#Given",["equality e_e","solveFor v_v"]), - ("#Where",["matches ((?a log ?v_) = ?b) e_e"]), + ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]), ("#Find" ,["solutions v_i"]), - ("#With" ,["||(lhs (Subst (v_i_,v_) e_e) - " ^ - " (rhs (Subst (v_i_,v_) e_e) || < eps)"]) + ("#With" ,["||(lhs (Subst (v_i_,v_v) e_e) - " ^ + " (rhs (Subst (v_i_,v_v) e_e) || < eps)"]) ], PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["Equation","solve_log"]])); @@ -45,7 +45,7 @@ (prep_met thy "met_equ_log" [] e_metID (["Equation","solve_log"], [("#Given" ,["equality e_e","solveFor v_v"]), - ("#Where" ,["matches ((?a log ?v_) = ?b) e_e"]), + ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]), ("#Find" ,["solutions v_i"]) ], {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,