| changeset 5192 | 704dd3a6d47d |
| parent 3323 | 194ae2e0c193 |
| child 12030 | 46d57d0290a2 |
--- a/src/HOLCF/Discrete0.thy Fri Jul 24 13:39:47 1998 +0200 +++ b/src/HOLCF/Discrete0.thy Fri Jul 24 13:44:27 1998 +0200 @@ -6,9 +6,9 @@ Discrete CPOs *) -Discrete0 = Cont + +Discrete0 = Cont + Datatype + -datatype 'a discr = Discr 'a +datatype 'a discr = Discr "'a :: term" instance discr :: (term)sq_ord