| author | wenzelm |
| Wed, 04 Dec 2013 18:59:20 +0100 | |
| changeset 54667 | 4dd08fe126ba |
| parent 42151 | 4da4fc77664b |
| child 58880 | 0baae4311a9f |
| permissions | -rw-r--r-- |
| 42151 | 1 |
(* Title: HOL/HOLCF/Library/HOL_Cpo.thy |
|
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
2 |
Author: Brian Huffman |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
3 |
*) |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
4 |
|
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
5 |
header {* Cpo class instances for all HOL types *}
|
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
6 |
|
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
7 |
theory HOL_Cpo |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
8 |
imports |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
9 |
Bool_Discrete |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
10 |
Nat_Discrete |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
11 |
Int_Discrete |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
12 |
Char_Discrete |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
13 |
Sum_Cpo |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
14 |
Option_Cpo |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
15 |
List_Predomain |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
16 |
begin |
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
17 |
|
|
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff
changeset
|
18 |
end |