src/HOL/NumberTheory/EvenOdd.thy

       also have "... = ((-1::int)^2)^ (nat a)";
         by (auto simp add: zpower_zpower [THEN sym])
       also have "(-1::int)^2 = 1";
         by auto
       finally; show ?thesis;
-        by (auto simp add: zpower_1)
+        by auto
     qed;
 qed;
 
 lemma neg_one_odd_power: "[| x \<in> zOdd; 0 \<le> x |] ==> (-1::int)^(nat x) = -1";
 proof -;

       also have "... = ((-1::int)^2)^ (nat a) * (-1)^1";
         by (auto simp add: zpower_zpower [THEN sym] zpower_zadd_distrib)
       also have "(-1::int)^2 = 1";
         by auto
       finally; show ?thesis;
-        by (auto simp add: zpower_1)
+        by auto
     qed;
 qed;
 
 lemma neg_one_power_parity: "[| 0 \<le> x; 0 \<le> y; (x \<in> zEven) = (y \<in> zEven) |] ==> 
   (-1::int)^(nat x) = (-1::int)^(nat y)";