(*
session Journal in Journal = "HOL" +
  options [ document_output = "..", document_variants="journal", document = pdf]
  sessions
    "HOL-Library"
  directories
     ".." 
  theories [document = false]
     "HOL-Library.LaTeXsugar"
     "HOL-Library.Sublist"
     "../Spec"
     "../Lexer"
     "../RegLangs"
     "../Simplifying"
     "../Sulzmann" 
     "../Positions"
     "../SizeBound"
  theories [document = true] 
     "Paper"
  document_files
     "root.bib"
     "root.tex"
     "llncs.cls"
*)

session Paper in Paper = "HOL" +
  options [ document_output = "..",
            document_build = "pdflatex",
	    document_variants="paper",
	    document = pdf,
	    document_heading_prefix = "",
	    document_comment_latex]
  sessions
    "HOL-Library"
  directories
     ".." 
  theories [document = false]
     "HOL-Library.LaTeXsugar"
     "HOL-Library.Sublist"
     "../Spec"
     "../Lexer"
     "../RegLangs"
     "../Simplifying"
     "../Sulzmann" 
     "../Positions"
     "../SizeBound4"
  theories [document = true] 
     "Paper"
  document_files
     "cc-by.pdf"
     "lipics-logo-bw.pdf"
     "root.bib"
     "root.tex"
     "lipics-v2021.cls"