| changeset 14348 | 744c868ee0b7 |
| parent 13871 | 26e5f5e624f6 |
| child 14434 | 5f14c1207499 |
--- a/src/HOL/NumberTheory/EvenOdd.thy Fri Jan 09 01:28:24 2004 +0100 +++ b/src/HOL/NumberTheory/EvenOdd.thy Fri Jan 09 10:46:18 2004 +0100 @@ -173,7 +173,7 @@ also have "(-1::int)^2 = 1"; by auto finally; show ?thesis; - by (auto simp add: zpower_1) + by auto qed; qed; @@ -199,7 +199,7 @@ also have "(-1::int)^2 = 1"; by auto finally; show ?thesis; - by (auto simp add: zpower_1) + by auto qed; qed;