author | huffman |
Mon, 08 Aug 2011 10:32:55 -0700 | |
changeset 44066 | d74182c93f04 |
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 |