equal
deleted
inserted
replaced
1 theory ToyList_Test |
1 theory ToyList_Test |
2 imports Main |
2 imports Main |
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML \<open> |
6 let val text = |
6 let val text = |
7 map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode) |
7 map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode) |
8 ["ToyList1.txt", "ToyList2.txt"] |
8 ["ToyList1.txt", "ToyList2.txt"] |
9 |> implode |
9 |> implode |
10 in Thy_Info.script_thy Position.start text @{theory} end |
10 in Thy_Info.script_thy Position.start text @{theory} end |
11 *} |
11 \<close> |
12 |
12 |
13 end |
13 end |