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