--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/Discrete.thy	Wed Mar 26 17:58:48 1997 +0100
@@ -0,0 +1,17 @@
+(*  Title:      HOLCF/Discrete.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TUM
+
+Discrete CPOs
+*)
+
+Discrete = Discrete1 +
+
+instance discr :: (term)cpo   (discr_cpo)
+
+constdefs
+   undiscr :: ('a::term)discr => 'a
+  "undiscr x == (case x of Discr y => y)"
+
+end