--- a/thys/Journal/Paper.thy	Sun Oct 10 00:56:47 2021 +0100
+++ b/thys/Journal/Paper.thy	Sun Oct 10 01:40:30 2021 +0100
@@ -1733,10 +1733,13 @@
   We can move out the @{term "fuse  [Z]"} and then use the IH to show that left-hand side
   and right-hand side are equal. This completes the proof. 
   \end{proof}   
-\<close>
 
 
 
+  \bibliographystyle{plain}
+  \bibliography{root}
+
+\<close>
 (*<*)
 end
 (*>*)
\ No newline at end of file

--- a/thys/Journal/document/root.tex	Sun Oct 10 00:56:47 2021 +0100
+++ b/thys/Journal/document/root.tex	Sun Oct 10 01:40:30 2021 +0100
@@ -13,7 +13,7 @@
 \usepackage{url}
 \usepackage{color}
 \usepackage[safe]{tipa}
-
+\usepackage{fontspec}
 
 
 \titlerunning{POSIX Lexing with Derivatives of Regular Expressions}

--- a/thys/ROOT	Sun Oct 10 00:56:47 2021 +0100
+++ b/thys/ROOT	Sun Oct 10 01:40:30 2021 +0100
@@ -2,7 +2,7 @@
 
 
 session Journal in Journal = "HOL" +
-  options [document_output = "..", document_variants="journal"]
+  options [ document_output = "..", document_variants="journal", document = pdf]
   sessions
     "HOL-Library"
   directories
@@ -20,4 +20,4 @@
      "Paper"
   document_files
      "root.bib"
-     "root.tex" 
\ No newline at end of file
+     "root.tex"
\ No newline at end of file

Binary file thys/journal.pdf has changed