--- a/src/HOL/Power.thy Thu Sep 16 15:32:24 2010 +0200 +++ b/src/HOL/Power.thy Thu Sep 16 15:37:12 2010 +0200 @@ -29,7 +29,7 @@ context monoid_mult begin -subclass power .. +subclass power . lemma power_one [simp]: "1 ^ n = 1"