src/Doc/Tutorial/ToyList/ToyList_Test.thy
author blanchet
Thu, 11 Sep 2014 18:54:36 +0200
changeset 58300 055afb5f7df8
parent 58112 8081087096ad
child 58372 bfd497f2f4c2
permissions -rw-r--r--
speed up old Nominal by killing type variables

theory ToyList_Test
imports Old_Datatype
begin

ML {*
  map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
    ["ToyList1.txt", "ToyList2.txt"]
  |> implode
  |> Thy_Info.script_thy Position.start
*}

end