src/Doc/Tutorial/ToyList/ToyList_Test.thy
author wenzelm
Sat Nov 10 19:39:38 2018 +0100 (11 months ago ago)
changeset 69287 94fa3376ba33
parent 67406 23307fd33906
child 69609 ff784d5a5bfb
permissions -rw-r--r--
added ML antiquotation @{master_dir};
     1 theory ToyList_Test
     2 imports Main
     3 begin
     4 
     5 ML \<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 
    12 end