src/HOLCF/ex/Dnat.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/ex/Dnat.thy	Fri Jan 31 16:56:32 1997 +0100
@@ -0,0 +1,19 @@
+(*  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