1.1 --- a/src/Tools/isac/Knowledge/LogExp.thy	Mon Sep 13 18:37:16 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy	Tue Sep 14 12:12:42 2010 +0200
     1.3 @@ -33,9 +33,9 @@
     1.4   (["logarithmic","univariate","equation"],
     1.5    [("#Given",["equality e_e","solveFor v_v"]),
     1.6     ("#Where",["matches ((?a log ?v_v) = ?b) e_e"]),
     1.7 -   ("#Find" ,["solutions v_i"]),
     1.8 -   ("#With" ,["||(lhs (Subst (v_i_,v_v) e_e) - " ^
     1.9 -	      "  (rhs (Subst (v_i_,v_v) e_e) || < eps)"])
    1.10 +   ("#Find" ,["solutions v_i'''"]),
    1.11 +   ("#With" ,["||(lhs (Subst (v_i''', v_v) e_e) - " ^
    1.12 +	      "  (rhs (Subst (v_i''', v_v) e_e) || < eps)"])
    1.13     ],
    1.14    PolyEq_prls, SOME "solve (e_e::bool, v_v)",
    1.15    [["Equation","solve_log"]]));
    1.16 @@ -47,7 +47,7 @@
    1.17   (["Equation","solve_log"],
    1.18    [("#Given" ,["equality e_e","solveFor v_v"]),
    1.19     ("#Where" ,["matches ((?a log ?v_v) = ?b) e_e"]),
    1.20 -   ("#Find"  ,["solutions v_i"])
    1.21 +   ("#Find"  ,["solutions v_i'''"])
    1.22    ],
    1.23     {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
    1.24      calc=[],crls=PolyEq_crls, nrls=norm_Rational},