
chapter AFP

session "RG_Locks" = HOL +

  options [
    timeout = 300
  ]

  sessions
    "HOL-Library"
    "HOL-Hoare"
    "HOL-Hoare_Parallel"
    "HOL-Eisbach"

  theories
    "RG_Syntax_Extensions"
    "RG_Annotated_Commands"
    "RG_Annotated_Methods"
    "RG_Examples_Reworked"
    "Helpers_Lists_Option"
    "Concurrent_Queue_Contract"
    "Lock_Abstract_Queue"
    "Lock_Ticket"
    "Lock_Circular_Buffer"

  document_files
    "root.tex"
    "root.bib"

