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