--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Discrete0.thy	Wed Mar 26 17:58:48 1997 +0100
@@ -0,0 +1,16 @@
+(*  Title:      HOLCF/Discrete0.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TUM
+
+Discrete CPOs
+*)
+
+Discrete0 = Cont +
+
+datatype 'a discr = Discr 'a
+
+defs
+less_discr_def "(less::('a::term)discr=>'a discr=>bool)  ==  op ="
+
+end