src/HOLCF/Discrete1.thy
author paulson
Fri, 21 Nov 2003 11:15:40 +0100
changeset 14265 95b42e69436c
parent 12338 de0f4a63baa5
child 14981 e73f8140af78
permissions -rw-r--r--
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     1
(*  Title:      HOLCF/Discrete1.thy
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     2
    ID:         $Id$
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
12030
wenzelm
parents: 2841
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     5
12030
wenzelm
parents: 2841
diff changeset
     6
Discrete CPOs.
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     7
*)
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     8
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     9
Discrete1 = Discrete0 +
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    10
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12030
diff changeset
    11
instance discr :: (type) po
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    12
  (less_discr_refl,less_discr_trans,less_discr_antisym)
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    13
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    14
end