src/HOLCF/Fix.thy
changeset 1410 324aa8134639
parent 1168 74be52691d62
child 1479 21eb5e156d91
--- a/src/HOLCF/Fix.thy	Mon Dec 18 13:09:17 1995 +0100
+++ b/src/HOLCF/Fix.thy	Wed Dec 20 16:28:51 1995 +0100
@@ -18,7 +18,7 @@
 adm          :: "('a=>bool)=>bool"
 admw         :: "('a=>bool)=>bool"
 chain_finite :: "'a=>bool"
-flat         :: "'a=>bool"
+is_flat         :: "'a=>bool"
 
 defs
 
@@ -35,7 +35,7 @@
 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