equal
deleted
inserted
replaced
53 |
53 |
54 constdefs |
54 constdefs |
55 zcongm :: "int => int => int => bool" |
55 zcongm :: "int => int => int => bool" |
56 "zcongm m == \<lambda>a b. zcong a b m" |
56 "zcongm m == \<lambda>a b. zcong a b m" |
57 |
57 |
58 lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = # -1)" |
58 lemma abs_eq_1_iff [iff]: "(abs z = (Numeral1::int)) = (z = Numeral1 \<or> z = -1)" |
59 -- {* LCP: not sure why this lemma is needed now *} |
59 -- {* LCP: not sure why this lemma is needed now *} |
60 apply (auto simp add: zabs_def) |
60 apply (auto simp add: zabs_def) |
61 done |
61 done |
62 |
62 |
63 |
63 |