src/HOLCF/Fix.thy
changeset 442 13ac1fd0a14d
parent 243 c22b85994e17
child 1150 66512c9e6bd6
--- a/src/HOLCF/Fix.thy	Wed Jun 29 12:01:17 1994 +0200
+++ b/src/HOLCF/Fix.thy	Wed Jun 29 12:03:41 1994 +0200
@@ -36,7 +36,7 @@
 \                        !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))"
 
 flat_def          "flat(x::'a) ==\
-\                        ! x y. x::'a << y --> (x = UU) | (x=y)"
+\                        ! x y. (x::'a) << y --> (x = UU) | (x=y)"
 
 end