src/HOL/Parity.thy
changeset 60562 24af00b010cf
parent 60343 063698416239
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Parity.thy	Mon Jun 22 23:19:48 2015 +0200
     1.2 +++ b/src/HOL/Parity.thy	Tue Jun 23 16:55:28 2015 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
     1.6  
     1.7 -class semiring_parity = comm_semiring_1_diff_distrib + numeral +
     1.8 +class semiring_parity = comm_semiring_1_cancel + numeral +
     1.9    assumes odd_one [simp]: "\<not> 2 dvd 1"
    1.10    assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
    1.11    assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"