# HG changeset patch
# User oheimb
# Date 842542086 -7200
# Node ID 9e23119c0219e669ea39c404dddcc6f8a90da984
# Parent  8e0ff1bfcfea00fd43b51842651d33d0f691f067
added comment on is_flat

diff -r 8e0ff1bfcfea -r 9e23119c0219 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Thu Sep 12 17:18:00 1996 +0200
+++ b/src/HOLCF/Fix.thy	Thu Sep 12 17:28:06 1996 +0200
@@ -12,13 +12,13 @@
 
 consts
 
-iterate :: "nat=>('a->'a)=>'a=>'a"
-Ifix    :: "('a->'a)=>'a"
-fix     :: "('a->'a)->'a"
-adm          :: "('a=>bool)=>bool"
-admw         :: "('a=>bool)=>bool"
-chain_finite :: "'a=>bool"
-is_flat         :: "'a=>bool"
+iterate	:: "nat=>('a->'a)=>'a=>'a"
+Ifix	:: "('a->'a)=>'a"
+fix	:: "('a->'a)->'a"
+adm		:: "('a=>bool)=>bool"
+admw		:: "('a=>bool)=>bool"
+chain_finite	:: "'a=>bool"
+is_flat		:: "'a=>bool" (* should be called flat, for consistency *)
 
 defs