src/HOL/Power.thy
changeset 39438 c5ece2a7a86e
parent 36409 d323e7773aa8
child 41550 efa734d9b221
     1.1 --- a/src/HOL/Power.thy	Thu Sep 16 15:32:24 2010 +0200
     1.2 +++ b/src/HOL/Power.thy	Thu Sep 16 15:37:12 2010 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  context monoid_mult
     1.5  begin
     1.6  
     1.7 -subclass power ..
     1.8 +subclass power .
     1.9  
    1.10  lemma power_one [simp]:
    1.11    "1 ^ n = 1"