equal
deleted
inserted
replaced
51 else 0)" |
51 else 0)" |
52 |
52 |
53 definition zcongm :: "int => int => int => bool" |
53 definition zcongm :: "int => int => int => bool" |
54 where "zcongm m = (\<lambda>a b. zcong a b m)" |
54 where "zcongm m = (\<lambda>a b. zcong a b m)" |
55 |
55 |
56 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)" |
56 lemma abs_eq_1_iff [iff]: "(\<bar>z\<bar> = (1::int)) = (z = 1 \<or> z = -1)" |
57 -- \<open>LCP: not sure why this lemma is needed now\<close> |
57 -- \<open>LCP: not sure why this lemma is needed now\<close> |
58 by (auto simp add: abs_if) |
58 by (auto simp add: abs_if) |
59 |
59 |
60 |
60 |
61 text \<open>\medskip @{text norRRset}\<close> |
61 text \<open>\medskip @{text norRRset}\<close> |