author | paulson |
Fri, 16 Nov 2001 18:24:11 +0100 | |
changeset 12224 | 02df7cbe7d25 |
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