| changeset 26289 | 9d2c375e242b |
| parent 22274 | ce1459004c8d |
| child 27651 | 16a26996c30e |
--- a/src/HOL/NumberTheory/EvenOdd.thy Sat Mar 15 22:07:28 2008 +0100 +++ b/src/HOL/NumberTheory/EvenOdd.thy Sat Mar 15 22:07:29 2008 +0100 @@ -249,7 +249,7 @@ lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |] ==> ((-1::int)^j = (-1::int)^k)" - using neg_one_power [of j] and insert neg_one_power [of k] + using neg_one_power [of j] and ListMem.insert neg_one_power [of k] by (auto simp add: one_not_neg_one_mod_m zcong_sym) end