src/HOL/Power.thy
changeset 31001 7e6ffd8f51a9
parent 30997 081e825c2218
child 31021 53642251a04f
     1.1 --- a/src/HOL/Power.thy	Mon Apr 27 08:22:37 2009 +0200
     1.2 +++ b/src/HOL/Power.thy	Mon Apr 27 10:11:44 2009 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    by (induct n) simp_all
     1.5  
     1.6  lemma power_one_right [simp]:
     1.7 -  "a ^ 1 = a * 1"
     1.8 +  "a ^ 1 = a"
     1.9    by simp
    1.10  
    1.11  lemma power_commutes: