1.1 --- a/src/Tools/isac/Knowledge/LogExp.thy	Mon Sep 06 15:53:18 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LogExp.thy	Mon Sep 06 16:56:22 2010 +0200
     1.3 @@ -17,12 +17,12 @@
     1.4  				    => bool list"
     1.5                    ("((Script Solve'_log (_ _=))//(_))" 9)
     1.6  
     1.7 -rules
     1.8 +axioms
     1.9  
    1.10 -  equality_pow    "0 < a ==> (l = r) = (a^^^l = a^^^r)"
    1.11 +  equality_pow:    "0 < a ==> (l = r) = (a^^^l = a^^^r)"
    1.12    (* this is what students   ^^^^^^^... are told to do *)
    1.13 -  equality_power  "((a log b) = c) = (a^^^(a log b) = a^^^c)"
    1.14 -  exp_invers_log  "a^^^(a log b) = b"
    1.15 +  equality_power:  "((a log b) = c) = (a^^^(a log b) = a^^^c)"
    1.16 +  exp_invers_log:  "a^^^(a log b) = b"
    1.17  
    1.18  ML {*
    1.19  val thy = @{theory};