# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1463478814 -3600
# Node ID 2e70c1b06ac0221af9b5d5bd41c36de34b3ebe5e
# Parent  162f112b814b2b486fec6ce5b7e62cae7a3a3266
updated

diff -r 162f112b814b -r 2e70c1b06ac0 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue May 17 05:14:41 2016 +0100
+++ b/thys/Paper/Paper.thy	Tue May 17 10:53:34 2016 +0100
@@ -445,7 +445,7 @@
 \begin{figure}[t]
 \begin{center}
 \begin{tikzpicture}[scale=2,node distance=1.3cm,
-                    every node/.style={minimum size=7mm}]
+                    every node/.style={minimum size=6mm}]
 \node (r1)  {@{term "r\<^sub>1"}};
 \node (r2) [right=of r1]{@{term "r\<^sub>2"}};
 \draw[->,line width=1mm](r1)--(r2) node[above,midway] {@{term "der a DUMMY"}};
@@ -465,6 +465,8 @@
 \draw (r4) node[anchor=north west] {\;\raisebox{-8mm}{@{term "mkeps"}}};
 \end{tikzpicture}
 \end{center}
+\mbox{}\\[-13mm]
+
 \caption{The two phases of the algorithm by Sulzmann \& Lu \cite{Sulzmann2014},
 matching the string @{term "[a,b,c]"}. The first phase (the arrows from 
 left to right) is \Brz's matcher building successive derivatives. If the 
@@ -1208,7 +1210,7 @@
   Having proved the correctness of the POSIX lexing algorithm in
   \cite{Sulzmann2014}, which lessons have we learned? Well, this is a
   perfect example for the importance of the \emph{right} definitions. We
-  have (on and off) banged our heads on doors as soon as first versions
+  have (on and off) explored mechanisations as soon as first versions
   of \cite{Sulzmann2014} appeared, but have made little progress with
   turning the relatively detailed proof sketch in \cite{Sulzmann2014} into a
   formalisable proof. Having seen \cite{Vansummeren2006} and adapted the
@@ -1216,7 +1218,7 @@
   the difference: the proofs, as said, are nearly straightforward. The
   question remains whether the original proof idea of \cite{Sulzmann2014},
   potentially using our result as a stepping stone, can be made to work?
-  Alas, we really do not know despite considerable effort and door banging.
+  Alas, we really do not know despite considerable effort.
 
 
   Closely related to our work is an automata-based lexer formalised by
diff -r 162f112b814b -r 2e70c1b06ac0 thys/Paper/document/root.bib
--- a/thys/Paper/document/root.bib	Tue May 17 05:14:41 2016 +0100
+++ b/thys/Paper/document/root.bib	Tue May 17 10:53:34 2016 +0100
@@ -34,7 +34,7 @@
 @book{Pierce2015,
   author = {B.~C.~Pierce and C.~Casinghino and M.~Gaboardi and
             M.~Greenberg and C.~Hri\c{t}cu and 
-            V.~Sjoberg and B.~Yorgey},
+            V.~Sj\"{o}berg and B.~Yorgey},
   title = {{S}oftware {F}oundations},
   year = {2015},
   publisher = {Electronic textbook},
diff -r 162f112b814b -r 2e70c1b06ac0 thys/paper.pdf
Binary file thys/paper.pdf has changed