1theory ToyList_Test 2imports Main 3begin 4 5ML \<open> 6 let val text = 7 map (File.read o Path.append \<^master_dir>) [\<^path>\<open>ToyList1.txt\<close>, \<^path>\<open>ToyList2.txt\<close>] 8 |> implode 9 in Thy_Info.script_thy Position.start text \<^theory> end 10\<close> 11 12end 13