# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1633826430 -3600
# Node ID fc346faada4e81f679c57bbf74e9a16dde0900ca
# Parent  e51c9a67a68de9797628652353b137e878fba29f
updated for Isabelle 2021

diff -r e51c9a67a68d -r fc346faada4e thys/Journal/Paper.thy
--- 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
diff -r e51c9a67a68d -r fc346faada4e thys/Journal/document/root.tex
--- 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}
diff -r e51c9a67a68d -r fc346faada4e thys/ROOT
--- 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
diff -r e51c9a67a68d -r fc346faada4e thys/journal.pdf
Binary file thys/journal.pdf has changed