author | haftmann |
Tue, 06 Oct 2009 20:00:08 +0200 | |
changeset 32882 | bfb3e24a4936 |
parent 30920 | 811ab0923a62 |
child 33591 | 51091e1041a7 |
permissions | -rw-r--r-- |
9000 | 1 |
(* Title: HOLCF/ex/ROOT.ML |
244 | 2 |
|
9000 | 3 |
Misc HOLCF examples. |
244 | 4 |
*) |
5 |
||
24106 | 6 |
use_thys ["Dnat", "Stream", "Dagstuhl", "Focus_ex", "Fix2", "Hoare", |
30920
811ab0923a62
add HOLCF/ex/Domain_ex.thy, with example uses of the domain package
huffman
parents:
29992
diff
changeset
|
7 |
"Loop", "Fixrec_ex", "Powerdomain_ex", "Domain_ex"]; |