diff -r 79b6cbd02681 -r b49723351533 src/Tools/isac/Knowledge/LogExp.thy
--- a/src/Tools/isac/Knowledge/LogExp.thy	Mon Sep 13 18:37:16 2010 +0200
+++ b/src/Tools/isac/Knowledge/LogExp.thy	Tue Sep 14 12:12:42 2010 +0200
@@ -33,9 +33,9 @@
  (["logarithmic","univariate","equation"],
   [("#Given",["equality e_e","solveFor v_v"]),
    ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
-   ("#Find" ,["solutions v_i"]),
-   ("#With" ,["||(lhs (Subst (v_i_,v_v) e_e) - " ^
-	      "  (rhs (Subst (v_i_,v_v) e_e) || < eps)"])
+   ("#Find" ,["solutions v_i'''"]),
+   ("#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"]]));
@@ -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_i'''"])
   ],
    {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
     calc=[],crls=PolyEq_crls, nrls=norm_Rational},