| changeset 15003 | 6145dd7538d7 |
| parent 14174 | f3cafd2929d5 |
| child 15197 | 19e735596e51 |
--- a/src/HOL/NumberTheory/EulerFermat.thy Thu Jun 24 17:51:28 2004 +0200 +++ b/src/HOL/NumberTheory/EulerFermat.thy Thu Jun 24 17:52:02 2004 +0200 @@ -60,7 +60,7 @@ lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)" -- {* LCP: not sure why this lemma is needed now *} -by (auto simp add: zabs_def) +by (auto simp add: abs_if) text {* \medskip @{text norRRset} *}