session "Lex" = HOL + theories [document = false] "ReStar" "Simplifying" "Sulzmann" session Paper in "Paper" = Lex + options [document = pdf, document_output = "..", document_variants="paper"] theories "~~/src/HOL/Library/LaTeXsugar" "Paper" document_files "root.bib" "root.tex"