src/HOL/NumberTheory/EvenOdd.thy
changeset 14348 744c868ee0b7
parent 13871 26e5f5e624f6
child 14434 5f14c1207499
     1.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Fri Jan 09 01:28:24 2004 +0100
     1.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Fri Jan 09 10:46:18 2004 +0100
     1.3 @@ -173,7 +173,7 @@
     1.4        also have "(-1::int)^2 = 1";
     1.5          by auto
     1.6        finally; show ?thesis;
     1.7 -        by (auto simp add: zpower_1)
     1.8 +        by auto
     1.9      qed;
    1.10  qed;
    1.11  
    1.12 @@ -199,7 +199,7 @@
    1.13        also have "(-1::int)^2 = 1";
    1.14          by auto
    1.15        finally; show ?thesis;
    1.16 -        by (auto simp add: zpower_1)
    1.17 +        by auto
    1.18      qed;
    1.19  qed;
    1.20