author | immler |
Sun, 27 Oct 2019 21:51:14 -0400 | |
changeset 71035 | 6fe5a0e1fa8e |
parent 41112 | 866148b76247 |
permissions | -rw-r--r-- |
37110
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff
changeset
|
1 |
theory HOLCF_Library |
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff
changeset
|
2 |
imports |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
40774
diff
changeset
|
3 |
Bool_Discrete |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
40774
diff
changeset
|
4 |
Char_Discrete |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
39143
diff
changeset
|
5 |
Defl_Bifinite |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
40774
diff
changeset
|
6 |
Int_Discrete |
39143 | 7 |
List_Cpo |
41112
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
40774
diff
changeset
|
8 |
List_Predomain |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
40774
diff
changeset
|
9 |
Nat_Discrete |
866148b76247
add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
40774
diff
changeset
|
10 |
Option_Cpo |
37110
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff
changeset
|
11 |
Stream |
37111 | 12 |
Sum_Cpo |
37110
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff
changeset
|
13 |
begin |
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff
changeset
|
14 |
|
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff
changeset
|
15 |
end |