author | huffman |
Wed, 17 Nov 2010 08:47:58 -0800 | |
changeset 40592 | f432973ce0f6 |
parent 39999 | e3948547b541 |
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 |
39999
e3948547b541
add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents:
39143
diff
changeset
|
3 |
Defl_Bifinite |
39143 | 4 |
List_Cpo |
37110
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff
changeset
|
5 |
Stream |
37111 | 6 |
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
|
7 |
begin |
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff
changeset
|
8 |
|
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff
changeset
|
9 |
end |