| changeset 1168 | 74be52691d62 |
| parent 442 | 13ac1fd0a14d |
| child 1479 | 21eb5e156d91 |
--- a/src/HOLCF/Fun2.thy Thu Jun 29 16:16:24 1995 +0200 +++ b/src/HOLCF/Fun2.thy Thu Jun 29 16:28:40 1995 +0200 @@ -24,7 +24,8 @@ inst_fun_po "((op <<)::['a=>'b::po,'a=>'b::po ]=>bool) = less_fun" -(* definitions *) +defs + (* The least element in type 'a::term => 'b::pcpo *) UU_fun_def "UU_fun == (% x.UU)"