author | wenzelm |
Wed, 05 Dec 2001 03:13:57 +0100 | |
changeset 12378 | 86c58273f8c0 |
parent 12196 | a3be6b3a9c0b |
child 14430 | 5cb24165a2e1 |
permissions | -rw-r--r-- |
(* 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