src/HOLCF/Discrete0.thy
author kleing
Mon, 21 Jun 2004 10:25:57 +0200
changeset 14981 e73f8140af78
parent 12338 de0f4a63baa5
permissions -rw-r--r--
Merged in license change from Isabelle2004
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/Discrete0.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
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     4
12030
wenzelm
parents: 5192
diff changeset
     5
Discrete CPOs.
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     6
*)
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     7
5192
704dd3a6d47d Adapted to new datatype package.
berghofe
parents: 3323
diff changeset
     8
Discrete0 = Cont + Datatype +
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
     9
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12030
diff changeset
    10
datatype 'a discr = Discr "'a :: type"
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    11
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12030
diff changeset
    12
instance discr :: (type) sq_ord
3323
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord
slotosch
parents: 2841
diff changeset
    13
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    14
defs
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12030
diff changeset
    15
less_discr_def "((op <<)::('a::type)discr=>'a discr=>bool)  ==  op ="
2841
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    16
c2508f4ab739 Added "discrete" CPOs and modified IMP to use those rather than "lift"
nipkow
parents:
diff changeset
    17
end