author | huffman |
Mon, 27 Apr 2009 19:44:30 -0700 | |
changeset 31008 | b8f4e351b5bf |
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"]; |