# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1462357777 -3600
# Node ID ca4dcfd912cbebbafcc17c70cb19b38a72f915e3
# Parent  15294ac95e47e332265eb8fa6e353e2e42a9ad82
updated literature

diff -r 15294ac95e47 -r ca4dcfd912cb Literature/PhdUpgradeReport.pdf
Binary file Literature/PhdUpgradeReport.pdf has changed
diff -r 15294ac95e47 -r ca4dcfd912cb Literature/better-parse-derivs.pdf
Binary file Literature/better-parse-derivs.pdf has changed
diff -r 15294ac95e47 -r ca4dcfd912cb Literature/kraus-nipkow-rexp.pdf
Binary file Literature/kraus-nipkow-rexp.pdf has changed
diff -r 15294ac95e47 -r ca4dcfd912cb Literature/pfenning-dfa16.pdf
Binary file Literature/pfenning-dfa16.pdf has changed
diff -r 15294ac95e47 -r ca4dcfd912cb Literature/spineless-tagless-gmachine.pdf
Binary file Literature/spineless-tagless-gmachine.pdf has changed
diff -r 15294ac95e47 -r ca4dcfd912cb Literature/tal-toplas.pdf
Binary file Literature/tal-toplas.pdf has changed
diff -r 15294ac95e47 -r ca4dcfd912cb thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Thu Apr 28 11:17:16 2016 +0100
+++ b/thys/Paper/Paper.thy	Wed May 04 11:29:37 2016 +0100
@@ -857,7 +857,7 @@
   \end{center}
 
   \noindent
-  The functions @{text "simp\<^bsub>ALT\<^esub>"} and @{text "simp\<^bsub>SEQ\<^esub>"} encode the simplification rules
+  The functions @{text "simp\<^bsub>Alt\<^esub>"} and @{text "simp\<^bsub>Seq\<^esub>"} encode the simplification rules
   and compose the rectification functions. The main simplification function is then 
 
   \begin{center}
diff -r 15294ac95e47 -r ca4dcfd912cb thys/paper.pdf
Binary file thys/paper.pdf has changed