--- a/src/HOLCF/Discrete.thy Fri Mar 04 23:23:47 2005 +0100 +++ b/src/HOLCF/Discrete.thy Fri Mar 04 23:25:06 2005 +0100 @@ -6,6 +6,8 @@ Discrete CPOs. *) +header {* Discrete cpo types *} + theory Discrete imports Cont Datatype begin