diff -r 3147f2c1525c -r f57ddfd09474 src/Tools/isac/Knowledge/LogExp.thy --- a/src/Tools/isac/Knowledge/LogExp.thy Thu Sep 23 08:43:36 2010 +0200 +++ b/src/Tools/isac/Knowledge/LogExp.thy Thu Sep 23 08:54:26 2010 +0200 @@ -33,7 +33,7 @@ (["logarithmic","univariate","equation"], [("#Given",["equality e_e","solveFor v_v"]), ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]), - ("#Find" ,["solutions v'i'"]), + ("#Find" ,["solutions v_v'i'"]), ("#With" ,["||(lhs (Subst (v'i', v_v) e_e) - " ^ " (rhs (Subst (v'i', v_v) e_e) || < eps)"]) ], @@ -47,7 +47,7 @@ (["Equation","solve_log"], [("#Given" ,["equality e_e","solveFor v_v"]), ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]), - ("#Find" ,["solutions v'i'"]) + ("#Find" ,["solutions v_v'i'"]) ], {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls, calc=[],crls=PolyEq_crls, nrls=norm_Rational},