src/HOLCF/Fix.thy

 Ifix    :: "('a->'a)=>'a"
 fix     :: "('a->'a)->'a"
 adm          :: "('a=>bool)=>bool"
 admw         :: "('a=>bool)=>bool"
 chain_finite :: "'a=>bool"
-flat         :: "'a=>bool"
+is_flat         :: "'a=>bool"
 
 defs
 
 iterate_def   "iterate n F c == nat_rec n c (%n x.F`x)"
 Ifix_def      "Ifix F == lub(range(%i.iterate i F UU))"

 			    P (lub(range (%i. iterate i F UU)))" 
 
 chain_finite_def  "chain_finite (x::'a)==
                         !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)"
 
-flat_def          "flat (x::'a) ==
+is_flat_def          "is_flat (x::'a) ==
                         ! x y. (x::'a) << y --> (x = UU) | (x=y)"
 
 end