src/HOLCF/Fix.thy

--- a/src/HOLCF/Fix.thy	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/Fix.thy	Fri Jul 24 13:44:27 1998 +0200
@@ -18,9 +18,12 @@
 adm		:: "('a::cpo=>bool)=>bool"
 admw		:: "('a=>bool)=>bool"
 
+primrec
+  iterate_0   "iterate 0 F x = x"
+  iterate_Suc "iterate (Suc n) F x  = F`(iterate n F x)"
+
 defs
 
-iterate_def   "iterate n F c == nat_rec c (%n x. F`x) n"
 Ifix_def      "Ifix F == lub(range(%i. iterate i F UU))"
 fix_def       "fix == (LAM f. Ifix f)"