src/HOL/NumberTheory/EvenOdd.thy
changeset 21404 eb85850d3eb7
parent 20369 7e03c3ed1a18
child 22274 ce1459004c8d
     1.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -8,9 +8,11 @@
     1.4  theory EvenOdd imports Int2 begin
     1.5  
     1.6  definition
     1.7 -  zOdd    :: "int set"
     1.8 +  zOdd    :: "int set" where
     1.9    "zOdd = {x. \<exists>k. x = 2 * k + 1}"
    1.10 -  zEven   :: "int set"
    1.11 +
    1.12 +definition
    1.13 +  zEven   :: "int set" where
    1.14    "zEven = {x. \<exists>k. x = 2 * k}"
    1.15  
    1.16  subsection {* Some useful properties about even and odd *}