src/HOL/Power.thy
changeset 58410 6d46ad54a2ab
parent 58157 c376c43c346c
child 58437 8d124c73c37a
     1.1 --- a/src/HOL/Power.thy	Sun Sep 21 16:56:06 2014 +0200
     1.2 +++ b/src/HOL/Power.thy	Sun Sep 21 16:56:11 2014 +0200
     1.3 @@ -214,7 +214,7 @@
     1.4    by (rule power_minus_Bit0)
     1.5  
     1.6  lemma power_minus1_even [simp]:
     1.7 -  "-1 ^ (2*n) = 1"
     1.8 +  "(- 1) ^ (2*n) = 1"
     1.9  proof (induct n)
    1.10    case 0 show ?case by simp
    1.11  next
    1.12 @@ -222,7 +222,7 @@
    1.13  qed
    1.14  
    1.15  lemma power_minus1_odd:
    1.16 -  "-1 ^ Suc (2*n) = -1"
    1.17 +  "(- 1) ^ Suc (2*n) = -1"
    1.18    by simp
    1.19  
    1.20  lemma power_minus_even [simp]: