src/HOL/Power.thy
changeset 61694 6571c78c9667
parent 61649 268d88ec9087
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Power.thy	Tue Nov 17 12:01:19 2015 +0100
     1.2 +++ b/src/HOL/Power.thy	Tue Nov 17 12:32:08 2015 +0000
     1.3 @@ -391,8 +391,6 @@
     1.4    "(a / b) ^ n = a ^ n / b ^ n"
     1.5    by (induct n) simp_all
     1.6  
     1.7 -declare power_divide [where b = "numeral w" for w, simp]
     1.8 -
     1.9  end
    1.10  
    1.11