author | wenzelm |
Wed, 25 Mar 2015 11:39:52 +0100 | |
changeset 59809 | 87641097d0f3 |
parent 58926 | baf5a3c28f0c |
child 67406 | 23307fd33906 |
permissions | -rw-r--r-- |
53376 | 1 |
theory ToyList_Test |
58926
baf5a3c28f0c
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents:
58856
diff
changeset
|
2 |
imports Main |
53376 | 3 |
begin |
4 |
||
57626 | 5 |
ML {* |
58856 | 6 |
let val text = |
7 |
map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode) |
|
8 |
["ToyList1.txt", "ToyList2.txt"] |
|
9 |
|> implode |
|
58926
baf5a3c28f0c
proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
wenzelm
parents:
58856
diff
changeset
|
10 |
in Thy_Info.script_thy Position.start text @{theory} end |
53376 | 11 |
*} |
12 |
||
13 |
end |