equal
deleted
inserted
replaced
58 zcongm :: "int => int => int => bool" |
58 zcongm :: "int => int => int => bool" |
59 "zcongm m == \<lambda>a b. zcong a b m" |
59 "zcongm m == \<lambda>a b. zcong a b m" |
60 |
60 |
61 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)" |
61 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)" |
62 -- {* LCP: not sure why this lemma is needed now *} |
62 -- {* LCP: not sure why this lemma is needed now *} |
63 by (auto simp add: zabs_def) |
63 by (auto simp add: abs_if) |
64 |
64 |
65 |
65 |
66 text {* \medskip @{text norRRset} *} |
66 text {* \medskip @{text norRRset} *} |
67 |
67 |
68 declare BnorRset.simps [simp del] |
68 declare BnorRset.simps [simp del] |