author | immler |
Sun, 27 Oct 2019 21:51:14 -0400 | |
changeset 71035 | 6fe5a0e1fa8e |
parent 62175 | 8ffc4d0e652d |
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 |
|
62175 | 5 |
section \<open>Cpo class instances for all HOL types\<close> |
41112
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 |