src/HOL/Hyperreal/EvenOdd.thy
author wenzelm
Wed, 05 Dec 2001 03:13:57 +0100
changeset 12378 86c58273f8c0
parent 12196 a3be6b3a9c0b
child 14430 5cb24165a2e1
permissions -rw-r--r--
removed bang_args;

(*  Title       : EvenOdd.thy
    Author      : Jacques D. Fleuriot  
    Copyright   : 1999  University of Edinburgh
    Description : Even and odd numbers defined 
*)

EvenOdd = NthRoot +  

consts even :: "nat => bool"
primrec 
   even_0   "even 0 = True"
   even_Suc "even (Suc n) = (~ (even n))"    

consts odd :: "nat => bool"
primrec 
   odd_0   "odd 0 = False"
   odd_Suc "odd (Suc n) = (~ (odd n))"    

end