src/HOL/Divides.thy
changeset 58710 7216a10d69ba
parent 58646 cd63a4b12a33
child 58778 e29cae8eab1f
     1.1 --- a/src/HOL/Divides.thy	Sun Oct 19 18:05:26 2014 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Oct 20 07:45:58 2014 +0200
     1.3 @@ -507,6 +507,7 @@
     1.4  class semiring_div_parity = semiring_div + semiring_numeral +
     1.5    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
     1.6    assumes one_mod_two_eq_one: "1 mod 2 = 1"
     1.7 +  assumes zero_not_eq_two: "0 \<noteq> 2"
     1.8  begin
     1.9  
    1.10  lemma parity_cases [case_names even odd]:
    1.11 @@ -573,6 +574,9 @@
    1.12  next
    1.13    show "1 mod 2 = 1"
    1.14      by (rule mod_less) simp_all
    1.15 +next
    1.16 +  show "0 \<noteq> 2"
    1.17 +    by simp
    1.18  qed
    1.19  
    1.20  lemma divmod_digit_1: