author | huffman |
Mon, 24 May 2010 11:29:49 -0700 | |
changeset 37109 | e67760c1b851 |
parent 37000 | 41a22e7c1145 |
child 37110 | 7ffdbc24b27f |
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", |
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", |
37109
e67760c1b851
move unused pattern match syntax stuff into HOLCF/ex
huffman
parents:
37000
diff
changeset
|
9 |
"Pattern_Match", |
37000
41a22e7c1145
move some example files into new HOLCF/Tutorial directory
huffman
parents:
35932
diff
changeset
|
10 |
"Strict_Fun"]; |