--- a/src/HOL/NumberTheory/EvenOdd.thy Wed May 17 01:23:40 2006 +0200
+++ b/src/HOL/NumberTheory/EvenOdd.thy Wed May 17 01:23:41 2006 +0200
@@ -7,20 +7,13 @@
theory EvenOdd imports Int2 begin
-text{*Note. This theory is being revised. See the web page
-\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
-
-constdefs
+definition
zOdd :: "int set"
- "zOdd == {x. \<exists>k. x = 2 * k + 1}"
+ "zOdd = {x. \<exists>k. x = 2 * k + 1}"
zEven :: "int set"
- "zEven == {x. \<exists>k. x = 2 * k}"
+ "zEven = {x. \<exists>k. x = 2 * k}"
-(***********************************************************)
-(* *)
-(* Some useful properties about even and odd *)
-(* *)
-(***********************************************************)
+subsection {* Some useful properties about even and odd *}
lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"