1
theory ToyList_Test
2
imports Datatype
3
begin
4
5
ML {*
6
map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
7
["ToyList1.txt", "ToyList2.txt"]
8
|> implode
9
|> Thy_Info.script_thy Position.start
10
*}
11
12
end
13