session UTM = HOL +
  options [document = false]
  theories
    "thys/Turing"
    "thys/Turing_Hoare"
    "thys/Uncomputable"
    "thys/Abacus_Mopup"
    "thys/Abacus"
    "thys/Rec_Def"
    "thys/Recursive"
    "thys/UF"
    "thys/UTM"

session ITP = UTM +
  options [document = pdf, document_output = "."]
  theories
    "Paper/Paper"