--- a/src/HOL/Power.thy Mon Apr 27 08:22:37 2009 +0200 +++ b/src/HOL/Power.thy Mon Apr 27 10:11:44 2009 +0200 @@ -36,7 +36,7 @@ by (induct n) simp_all lemma power_one_right [simp]: - "a ^ 1 = a * 1" + "a ^ 1 = a" by simp lemma power_commutes: