author | huffman |
Mon, 24 May 2010 12:10:24 -0700 | |
changeset 37110 | 7ffdbc24b27f |
parent 37109 | e67760c1b851 |
permissions | -rw-r--r-- |
9000 | 1 |
(* Title: HOLCF/ex/ROOT.ML |
244 | 2 |
|
9000 | 3 |
Misc HOLCF examples. |
244 | 4 |
*) |
5 |
||
37110
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
37109
diff
changeset
|
6 |
use_thys ["Dnat", "Dagstuhl", "Focus_ex", "Fix2", "Hoare", |
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset
|
7 |
"Loop", "Powerdomain_ex", "Domain_Proofs", |
35932
86559356502d
move letrec stuff to new file HOLCF/ex/Letrec.thy
huffman
parents:
35167
diff
changeset
|
8 |
"Letrec", |
37110
7ffdbc24b27f
move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
37109
diff
changeset
|
9 |
"Pattern_Match"]; |