| author | haftmann |
| Mon, 04 May 2009 14:49:46 +0200 | |
| changeset 31031 | cbec39ebf8f2 |
| 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"]; |