src/HOLCF/Discrete.thy

add_defs(_i): overloaded option;

+
−(*  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