src/HOL/NumberTheory/EvenOdd.thy
changeset 19670 2e4a143c73c5
parent 18369 694ea14ab4f2
child 20369 7e03c3ed1a18
     1.1 --- a/src/HOL/NumberTheory/EvenOdd.thy	Wed May 17 01:23:40 2006 +0200
     1.2 +++ b/src/HOL/NumberTheory/EvenOdd.thy	Wed May 17 01:23:41 2006 +0200
     1.3 @@ -7,20 +7,13 @@
     1.4  
     1.5  theory EvenOdd imports Int2 begin
     1.6  
     1.7 -text{*Note.  This theory is being revised.  See the web page
     1.8 -\url{http://www.andrew.cmu.edu/~avigad/isabelle}.*}
     1.9 -
    1.10 -constdefs
    1.11 +definition
    1.12    zOdd    :: "int set"
    1.13 -  "zOdd == {x. \<exists>k. x = 2 * k + 1}"
    1.14 +  "zOdd = {x. \<exists>k. x = 2 * k + 1}"
    1.15    zEven   :: "int set"
    1.16 -  "zEven == {x. \<exists>k. x = 2 * k}"
    1.17 +  "zEven = {x. \<exists>k. x = 2 * k}"
    1.18  
    1.19 -(***********************************************************)
    1.20 -(*                                                         *)
    1.21 -(* Some useful properties about even and odd               *)
    1.22 -(*                                                         *)
    1.23 -(***********************************************************)
    1.24 +subsection {* Some useful properties about even and odd *}
    1.25  
    1.26  lemma zOddI [intro?]: "x = 2 * k + 1 \<Longrightarrow> x \<in> zOdd"
    1.27    and zOddE [elim?]: "x \<in> zOdd \<Longrightarrow> (!!k. x = 2 * k + 1 \<Longrightarrow> C) \<Longrightarrow> C"