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