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};
wenzelm@53376
     1
theory ToyList_Test
wenzelm@58926
     2
imports Main
wenzelm@53376
     3
begin
wenzelm@53376
     4
wenzelm@67406
     5
ML \<open>
wenzelm@58856
     6
  let val text =
wenzelm@69287
     7
    map (File.read o Path.append \<^master_dir>) [\<^path>\<open>ToyList1.txt\<close>, \<^path>\<open>ToyList2.txt\<close>]
wenzelm@58856
     8
    |> implode
wenzelm@58926
     9
  in Thy_Info.script_thy Position.start text @{theory} end
wenzelm@67406
    10
\<close>
wenzelm@53376
    11
wenzelm@53376
    12
end