| author | wenzelm |
| Thu Aug 27 20:46:36 1998 +0200 (1998-08-27) | |
| changeset 5400 | 645f46a24c72 |
| parent 5192 | 704dd3a6d47d |
| child 12030 | 46d57d0290a2 |
| permissions | -rw-r--r-- |
| nipkow@2841 | 1 |
(* Title: HOLCF/Discrete0.thy |
| nipkow@2841 | 2 |
ID: $Id$ |
| nipkow@2841 | 3 |
Author: Tobias Nipkow |
| nipkow@2841 | 4 |
Copyright 1997 TUM |
| nipkow@2841 | 5 |
|
| nipkow@2841 | 6 |
Discrete CPOs |
| nipkow@2841 | 7 |
*) |
| nipkow@2841 | 8 |
|
| berghofe@5192 | 9 |
Discrete0 = Cont + Datatype + |
| nipkow@2841 | 10 |
|
| berghofe@5192 | 11 |
datatype 'a discr = Discr "'a :: term" |
| nipkow@2841 | 12 |
|
| slotosch@3323 | 13 |
instance discr :: (term)sq_ord |
| slotosch@3323 | 14 |
|
| nipkow@2841 | 15 |
defs |
| slotosch@3323 | 16 |
less_discr_def "((op <<)::('a::term)discr=>'a discr=>bool) == op ="
|
| nipkow@2841 | 17 |
|
| nipkow@2841 | 18 |
end |