author | nipkow |
Tue, 09 Jan 2001 15:36:30 +0100 | |
changeset 10835 | f4745d77e620 |
parent 2570 | 24d7e8fb8261 |
child 12035 | f2ee4b5d02f2 |
permissions | -rw-r--r-- |
(* Title: HOLCF/Dnat.thy ID: $Id$ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen Theory for the domain of natural numbers dnat = one ++ dnat *) Dnat = HOLCF + domain dnat = dzero | dsucc (dpred :: dnat) constdefs iterator :: "dnat -> ('a -> 'a) -> 'a -> 'a" "iterator == fix$(LAM h n f x . case n of dzero => x | dsucc$m => f$(h$m$f$x))" end