| changeset 22274 | ce1459004c8d |
| parent 21404 | eb85850d3eb7 |
| child 26289 | 9d2c375e242b |
--- a/src/HOL/NumberTheory/EvenOdd.thy Wed Feb 07 17:46:03 2007 +0100 +++ b/src/HOL/NumberTheory/EvenOdd.thy Wed Feb 07 17:51:38 2007 +0100 @@ -242,7 +242,7 @@ lemma neg_one_special: "finite A ==> ((-1 :: int) ^ card A) * (-1 ^ card A) = 1" - by (induct set: Finites) auto + by (induct set: finite) auto lemma neg_one_power: "(-1::int)^n = 1 | (-1::int)^n = -1" by (induct n) auto