src/HOL/Parity.thy
changeset 61799 4cf66f21b764
parent 61531 ab2e862263e7
child 62083 7582b39f51ed
     1.1 --- a/src/HOL/Parity.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Parity.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  imports Nat_Transfer
     1.5  begin
     1.6  
     1.7 -subsection \<open>Ring structures with parity and @{text even}/@{text odd} predicates\<close>
     1.8 +subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
     1.9  
    1.10  class semiring_parity = comm_semiring_1_cancel + numeral +
    1.11    assumes odd_one [simp]: "\<not> 2 dvd 1"