session "Hoare_gen" in "thys" = "HOL" ++
−
  theories +
−
     Hoare_gen+
−
+
−
session "Hoare_tm" in "thys" = "Hoare_gen" ++
−
  theories +
−
     Hoare_tm+
−
+
−
session "Hoare_abc" in "thys" = "Hoare_tm" ++
−
  theories+
−
     Hoare_abc+
−
+
−
session "TM" in "thys" = Hoare_abc ++
−
  theories +
−
    My_block+
−
    LetElim+
−
    AList+
−
    StateMonad+
−
    TM_Assemble+
−
+
−
session "Paper" in "paper" = TM ++
−
  options [document = pdf, document_output = "..", document_variants = "journal"]+
−
  theories+
−
    Paper+
−
  files "document/root.tex"+
−