isabelle: src/HOL/Hyperreal/EvenOdd.thy@a3be6b3a9c0b (annotated)

12196 a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	1	(* Title : EvenOdd.thy
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	2	Author : Jacques D. Fleuriot
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	3	Copyright : 1999 University of Edinburgh
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	4	Description : Even and odd numbers defined
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	5	*)
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	6
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	7	EvenOdd = NthRoot +
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	8
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	9	consts even :: "nat => bool"
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	10	primrec
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	11	even_0 "even 0 = True"
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	12	even_Suc "even (Suc n) = (~ (even n))"
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	13
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	14	consts odd :: "nat => bool"
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	15	primrec
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	16	odd_0 "odd 0 = False"
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	17	odd_Suc "odd (Suc n) = (~ (odd n))"
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	18
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	19	end
a3be6b3a9c0b new theories from Jacques Fleuriot paulson parents: diff changeset	20

author	paulson
	Thu, 15 Nov 2001 16:12:49 +0100
changeset 12196	a3be6b3a9c0b
child 14430	5cb24165a2e1
permissions	-rw-r--r--