--- a/thys/Paper/Paper.thy	Mon May 09 15:01:31 2016 +0100
+++ b/thys/Paper/Paper.thy	Wed May 11 12:20:16 2016 +0100
@@ -102,50 +102,6 @@
 of the work by Krauss and Nipkow \cite{Krauss2011}. And another one in Coq is given
 by Coquand and Siles \cite{Coquand2012}.
 
-One limitation of Brzozowski's matcher is that it only generates a
-YES/NO answer for whether a string is being matched by a regular
-expression.  Sulzmann and Lu \cite{Sulzmann2014} extended this matcher
-to allow generation not just of a YES/NO answer but of an actual
-matching, called a [lexical] {\em value}. They give a simple algorithm
-to calculate a value that appears to be the value associated with
-POSIX matching. The challenge then is to specify that value, in an
-algorithm-independent fashion, and to show that Sulzmann and Lu's
-derivative-based algorithm does indeed calculate a value that is
-correct according to the specification.
-
-The answer given by Sulzmann and Lu \cite{Sulzmann2014} is to define a
-relation (called an ``order relation'') on the set of values of @{term
-r}, and to show that (once a string to be matched is chosen) there is
-a maximum element and that it is computed by their derivative-based
-algorithm. This proof idea is inspired by work of Frisch and Cardelli
-\cite{Frisch2004} on a GREEDY regular expression matching
-algorithm. However, we were not able to establish transitivity and
-totality for the ``order relation'' by Sulzmann and Lu. In Section
-\ref{argu} we identify some inherent problems with their approach (of
-which some of the proofs are not published in \cite{Sulzmann2014});
-perhaps more importantly, we give a simple inductive (and
-algorithm-independent) definition of what we call being a {\em POSIX
-value} for a regular expression @{term r} and a string @{term s}; we
-show that the algorithm computes such a value and that such a value is
-unique. Proofs are both done by hand and checked in Isabelle/HOL.  The
-experience of doing our proofs has been that this mechanical checking
-was absolutely essential: this subject area has hidden snares. This
-was also noted by Kuklewicz \cite{Kuklewicz} who found that nearly all
-POSIX matching implementations are ``buggy'' \cite[Page
-203]{Sulzmann2014}.
-
-%\footnote{The relation @{text "\<ge>\<^bsub>r\<^esub>"} defined by Sulzmann and Lu \cite{Sulzmann2014} 
-%is a relation on the
-%values for the regular expression @{term r}; but it only holds between
-%@{term "v\<^sub>1"} and @{term "v\<^sub>2"} in cases where @{term "v\<^sub>1"} and @{term "v\<^sub>2"} have
-%the same flattening (underlying string). So a counterexample to totality is
-%given by taking two values @{term "v\<^sub>1"} and @{term "v\<^sub>2"} for @{term r} that
-%have different flattenings (see Section~\ref{posixsec}). A different
-%relation @{text "\<ge>\<^bsub>r,s\<^esub>"} on the set of values for @{term r}
-%with flattening @{term s} is definable by the same approach, and is indeed
-%total; but that is not what Proposition 1 of \cite{Sulzmann2014} does.}
-
-
 If a regular expression matches a string, then in general there is more than
 one way of how the string is matched. There are two commonly used
 disambiguation strategies to generate a unique answer: one is called GREEDY
@@ -170,26 +126,76 @@
 expressions:
 
 \begin{itemize} 
-\item[$\bullet$] \underline{The Longest Match Rule (or ``maximal munch rule''):}\smallskip
-
+\item[$\bullet$] \emph{The Longest Match Rule} (or \emph{``maximal munch rule''}):
 The longest initial substring matched by any regular expression is taken as
 next token.\smallskip
 
-\item[$\bullet$] \underline{Priority Rule:}\smallskip
-
+\item[$\bullet$] \emph{Priority Rule:}
 For a particular longest initial substring, the first regular expression
 that can match determines the token.
 \end{itemize}
- 
-\noindent Consider for example @{text "r\<^bsub>key\<^esub>"} recognising keywords such as
-@{text "if"}, @{text "then"} and so on; and @{text "r\<^bsub>id\<^esub>"} recognising
-identifiers (say, a single character followed by characters or numbers).
-Then we can form the regular expression @{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} and use
-POSIX matching to tokenise strings, say @{text "iffoo"} and @{text "if"}.
-For @{text "iffoo"} we obtain by the longest match rule a single identifier
-token, not a keyword followed by an identifier. For @{text "if"} we obtain by
-the priority rule a keyword token, not an identifier token---even if @{text
-"r\<^bsub>id\<^esub>"} matches also.\bigskip
+
+\noindent Consider for example @{text "r\<^bsub>key\<^esub>"} recognising keywords
+such as @{text "if"}, @{text "then"} and so on; and @{text "r\<^bsub>id\<^esub>"}
+recognising identifiers (say, a single character followed by
+characters or numbers).  Then we can form the regular expression
+@{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} and use POSIX matching to tokenise strings,
+say @{text "iffoo"} and @{text "if"}.  For @{text "iffoo"} we obtain
+by the Longest Match Rule a single identifier token, not a keyword
+followed by an identifier. For @{text "if"} we obtain by the Priority
+Rule a keyword token, not an identifier token---even if @{text "r\<^bsub>id\<^esub>"}
+matches also.
+
+One limitation of Brzozowski's matcher is that it only generates a
+YES/NO answer for whether a string is being matched by a regular
+expression.  Sulzmann and Lu~\cite{Sulzmann2014} extended this matcher
+to allow generation not just of a YES/NO answer but of an actual
+matching, called a [lexical] {\em value}. They give a simple algorithm
+to calculate a value that appears to be the value associated with
+POSIX matching.  The challenge then is to specify that value, in an
+algorithm-independent fashion, and to show that Sulzmann and Lu's
+derivative-based algorithm does indeed calculate a value that is
+correct according to the specification.
+
+The answer given by Sulzmann and Lu \cite{Sulzmann2014} is to define a
+relation (called an ``order relation'') on the set of values of @{term
+r}, and to show that (once a string to be matched is chosen) there is
+a maximum element and that it is computed by their derivative-based
+algorithm. This proof idea is inspired by work of Frisch and Cardelli
+\cite{Frisch2004} on a GREEDY regular expression matching
+algorithm. However, we were not able to establish transitivity and
+totality for the ``order relation'' by Sulzmann and Lu. In Section
+\ref{argu} we identify some inherent problems with their approach (of
+which some of the proofs are not published in \cite{Sulzmann2014});
+perhaps more importantly, we give a simple inductive (and
+algorithm-independent) definition of what we call being a {\em POSIX
+value} for a regular expression @{term r} and a string @{term s}; we
+show that the algorithm computes such a value and that such a value is
+unique. Our proofs are both done by hand and checked in Isabelle/HOL.  The
+experience of doing our proofs has been that this mechanical checking
+was absolutely essential: this subject area has hidden snares. This
+was also noted by Kuklewicz \cite{Kuklewicz} who found that nearly all
+POSIX matching implementations are ``buggy'' \cite[Page
+203]{Sulzmann2014} and by Grathwohl et al \cite[Page 36]{CrashCourse2014}
+who wrote:
+
+\begin{quote}
+\it{}``The POSIX strategy is more complicated than the greedy because of 
+the dependence on information about the length of matched strings in the 
+various subexpressions.''
+\end{quote}
+
+%\footnote{The relation @{text "\<ge>\<^bsub>r\<^esub>"} defined by Sulzmann and Lu \cite{Sulzmann2014} 
+%is a relation on the
+%values for the regular expression @{term r}; but it only holds between
+%@{term "v\<^sub>1"} and @{term "v\<^sub>2"} in cases where @{term "v\<^sub>1"} and @{term "v\<^sub>2"} have
+%the same flattening (underlying string). So a counterexample to totality is
+%given by taking two values @{term "v\<^sub>1"} and @{term "v\<^sub>2"} for @{term r} that
+%have different flattenings (see Section~\ref{posixsec}). A different
+%relation @{text "\<ge>\<^bsub>r,s\<^esub>"} on the set of values for @{term r}
+%with flattening @{term s} is definable by the same approach, and is indeed
+%total; but that is not what Proposition 1 of \cite{Sulzmann2014} does.}
+
 
 \noindent {\bf Contributions:} We have implemented in Isabelle/HOL the
 derivative-based regular expression matching algorithm of
@@ -239,10 +245,13 @@
   recursive function @{term L} with the clauses:
 
   \begin{center}
-  \begin{tabular}{l@ {\hspace{5mm}}rcl}
+  \begin{tabular}{l@ {\hspace{3mm}}rcl}
   (1) & @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\
   (2) & @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\
   (3) & @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\
+  \end{tabular}
+  \hspace{14mm}
+  \begin{tabular}{l@ {\hspace{3mm}}rcl}
   (4) & @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
   (5) & @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\
   (6) & @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\
@@ -355,11 +364,11 @@
 
 text {* 
 
-  The clever idea by Sulzmann and Lu \cite{Sulzmann2014} is to introduce values for encoding
-  \emph{how} a regular expression matches a string and then define a
-  function on values that mirrors (but inverts) the construction of the
-  derivative on regular expressions. \emph{Values} are defined as the
-  inductive datatype
+  The clever idea by Sulzmann and Lu \cite{Sulzmann2014} is to define
+  values for encoding \emph{how} a regular expression matches a string
+  and then define a function on values that mirrors (but inverts) the
+  construction of the derivative on regular expressions. \emph{Values}
+  are defined as the inductive datatype
 
   \begin{center}
   @{text "v :="}
@@ -379,11 +388,13 @@
   @{term "flat DUMMY"} and defined as:
 
   \begin{center}
-  \begin{tabular}{lcl}
+  \begin{tabular}[t]{lcl}
   @{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\
   @{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\
   @{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\
-  @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}\\
+  @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}
+  \end{tabular}\hspace{14mm}
+  \begin{tabular}[t]{lcl}
   @{thm (lhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\
   @{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\
   @{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\
@@ -395,11 +406,12 @@
 
   \begin{center}
   \begin{tabular}{c}
+  \\[-8mm]
   @{thm[mode=Axiom] Prf.intros(4)} \qquad
-  @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\smallskip\\
+  @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[3mm]
   @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad 
-  @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\smallskip\\
-  @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\smallskip\\ 
+  @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[3mm]
+  @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[3mm]
   @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad  
   @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}
   \end{tabular}

--- a/thys/Paper/document/llncs.cls	Mon May 09 15:01:31 2016 +0100
+++ b/thys/Paper/document/llncs.cls	Wed May 11 12:20:16 2016 +0100
@@ -1,4 +1,4 @@
-% LLNCS DOCUMENT CLASS -- version 2.13 (28-Jan-2002)
+% LLNCS DOCUMENT CLASS -- version 2.19 (31-Mar-2014)
 % Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
 %
 %%
@@ -19,7 +19,7 @@
 %%   Right brace   \}     Tilde         \~}
 %%
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesClass{llncs}[2002/01/28 v2.13
+\ProvidesClass{llncs}[2014/03/31 v2.19
 ^^J LaTeX document class for Lecture Notes in Computer Science]
 % Options
 \let\if@envcntreset\iffalse
@@ -35,6 +35,7 @@
 \let\if@runhead\iffalse
 \DeclareOption{runningheads}{\let\if@runhead\iftrue}
 
+\let\if@openright\iftrue
 \let\if@openbib\iffalse
 \DeclareOption{openbib}{\let\if@openbib\iftrue}
 
@@ -49,6 +50,7 @@
 
 \LoadClass[twoside]{article}
 \RequirePackage{multicol} % needed for the list of participants, index
+\RequirePackage{aliascnt}
 
 \setlength{\textwidth}{12.2cm}
 \setlength{\textheight}{19.3cm}
@@ -75,40 +77,40 @@
   \fi}
 %
 \def\switcht@albion{%
-\def\abstractname{Abstract.}
-\def\ackname{Acknowledgement.}
-\def\andname{and}
-\def\lastandname{\unskip, and}
-\def\appendixname{Appendix}
-\def\chaptername{Chapter}
-\def\claimname{Claim}
-\def\conjecturename{Conjecture}
-\def\contentsname{Table of Contents}
-\def\corollaryname{Corollary}
-\def\definitionname{Definition}
-\def\examplename{Example}
-\def\exercisename{Exercise}
-\def\figurename{Fig.}
-\def\keywordname{{\bf Key words:}}
-\def\indexname{Index}
-\def\lemmaname{Lemma}
-\def\contriblistname{List of Contributors}
-\def\listfigurename{List of Figures}
-\def\listtablename{List of Tables}
-\def\mailname{{\it Correspondence to\/}:}
-\def\noteaddname{Note added in proof}
-\def\notename{Note}
-\def\partname{Part}
-\def\problemname{Problem}
-\def\proofname{Proof}
-\def\propertyname{Property}
-\def\propositionname{Proposition}
-\def\questionname{Question}
-\def\remarkname{Remark}
-\def\seename{see}
-\def\solutionname{Solution}
-\def\subclassname{{\it Subject Classifications\/}:}
-\def\tablename{Table}
+\def\abstractname{Abstract.}%
+\def\ackname{Acknowledgement.}%
+\def\andname{and}%
+\def\lastandname{\unskip, and}%
+\def\appendixname{Appendix}%
+\def\chaptername{Chapter}%
+\def\claimname{Claim}%
+\def\conjecturename{Conjecture}%
+\def\contentsname{Table of Contents}%
+\def\corollaryname{Corollary}%
+\def\definitionname{Definition}%
+\def\examplename{Example}%
+\def\exercisename{Exercise}%
+\def\figurename{Fig.}%
+\def\keywordname{{\bf Keywords:}}%
+\def\indexname{Index}%
+\def\lemmaname{Lemma}%
+\def\contriblistname{List of Contributors}%
+\def\listfigurename{List of Figures}%
+\def\listtablename{List of Tables}%
+\def\mailname{{\it Correspondence to\/}:}%
+\def\noteaddname{Note added in proof}%
+\def\notename{Note}%
+\def\partname{Part}%
+\def\problemname{Problem}%
+\def\proofname{Proof}%
+\def\propertyname{Property}%
+\def\propositionname{Proposition}%
+\def\questionname{Question}%
+\def\remarkname{Remark}%
+\def\seename{see}%
+\def\solutionname{Solution}%
+\def\subclassname{{\it Subject Classifications\/}:}%
+\def\tablename{Table}%
 \def\theoremname{Theorem}}
 \switcht@albion
 % Names of theorem like environments are already defined
@@ -120,7 +122,7 @@
  \def\ackname{Remerciements.}%
  \def\andname{et}%
  \def\lastandname{ et}%
- \def\appendixname{Appendice}
+ \def\appendixname{Appendice}%
  \def\chaptername{Chapitre}%
  \def\claimname{Pr\'etention}%
  \def\conjecturename{Hypoth\`ese}%
@@ -130,13 +132,13 @@
  \def\examplename{Exemple}%
  \def\exercisename{Exercice}%
  \def\figurename{Fig.}%
- \def\keywordname{{\bf Mots-cl\'e:}}
- \def\indexname{Index}
+ \def\keywordname{{\bf Mots-cl\'e:}}%
+ \def\indexname{Index}%
  \def\lemmaname{Lemme}%
- \def\contriblistname{Liste des contributeurs}
+ \def\contriblistname{Liste des contributeurs}%
  \def\listfigurename{Liste des figures}%
  \def\listtablename{Liste des tables}%
- \def\mailname{{\it Correspondence to\/}:}
+ \def\mailname{{\it Correspondence to\/}:}%
  \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
  \def\notename{Remarque}%
  \def\partname{Partie}%
@@ -146,9 +148,9 @@
 %\def\propositionname{Proposition}%
  \def\questionname{Question}%
  \def\remarkname{Remarque}%
- \def\seename{voir}
+ \def\seename{voir}%
  \def\solutionname{Solution}%
- \def\subclassname{{\it Subject Classifications\/}:}
+ \def\subclassname{{\it Subject Classifications\/}:}%
  \def\tablename{Tableau}%
  \def\theoremname{Th\'eor\`eme}%
 }
@@ -169,13 +171,13 @@
  \def\examplename{Beispiel}%
  \def\exercisename{\"Ubung}%
  \def\figurename{Abb.}%
- \def\keywordname{{\bf Schl\"usselw\"orter:}}
- \def\indexname{Index}
+ \def\keywordname{{\bf Schl\"usselw\"orter:}}%
+ \def\indexname{Index}%
 %\def\lemmaname{Lemma}%
- \def\contriblistname{Mitarbeiter}
+ \def\contriblistname{Mitarbeiter}%
  \def\listfigurename{Abbildungsverzeichnis}%
  \def\listtablename{Tabellenverzeichnis}%
- \def\mailname{{\it Correspondence to\/}:}
+ \def\mailname{{\it Correspondence to\/}:}%
  \def\noteaddname{Nachtrag}%
  \def\notename{Anmerkung}%
  \def\partname{Teil}%
@@ -185,9 +187,9 @@
 %\def\propositionname{Proposition}%
  \def\questionname{Frage}%
  \def\remarkname{Anmerkung}%
- \def\seename{siehe}
+ \def\seename{siehe}%
  \def\solutionname{L\"osung}%
- \def\subclassname{{\it Subject Classifications\/}:}
+ \def\subclassname{{\it Subject Classifications\/}:}%
  \def\tablename{Tabelle}%
 %\def\theoremname{Theorem}%
 }
@@ -539,23 +541,29 @@
 
 \def\@dotsep{2}
 
+\let\phantomsection=\relax
+
 \def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
-{chapter.\thechapter}\fi}
+{}\fi}
 
 \def\addnumcontentsmark#1#2#3{%
 \addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
-                     {\thechapter}#3}{\thepage}\hyperhrefextend}}
+                     {\thechapter}#3}{\thepage}\hyperhrefextend}}%
 \def\addcontentsmark#1#2#3{%
-\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}%
 \def\addcontentsmarkwop#1#2#3{%
-\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}%
 
 \def\@adcmk[#1]{\ifcase #1 \or
 \def\@gtempa{\addnumcontentsmark}%
   \or    \def\@gtempa{\addcontentsmark}%
   \or    \def\@gtempa{\addcontentsmarkwop}%
-  \fi\@gtempa{toc}{chapter}}
-\def\addtocmark{\@ifnextchar[{\@adcmk}{\@adcmk[3]}}
+  \fi\@gtempa{toc}{chapter}%
+}
+\def\addtocmark{%
+\phantomsection
+\@ifnextchar[{\@adcmk}{\@adcmk[3]}%
+}
 
 \def\l@chapter#1#2{\addpenalty{-\@highpenalty}
  \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
@@ -587,7 +595,7 @@
  \penalty\@highpenalty \endgroup}
 
 \def\l@author#1#2{\addpenalty{\@highpenalty}
- \@tempdima=\z@ %15\p@
+ \@tempdima=15\p@ %\z@
  \begingroup
  \parindent \z@ \rightskip \@tocrmarg
  \advance\rightskip by 0pt plus 2cm
@@ -596,7 +604,7 @@
  \textit{#1}\par
  \penalty\@highpenalty \endgroup}
 
-%\setcounter{tocdepth}{0}
+\setcounter{tocdepth}{0}
 \newdimen\tocchpnum
 \newdimen\tocsecnum
 \newdimen\tocsectotal
@@ -779,6 +787,7 @@
     \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
 
 \long\def\@makecaption#1#2{%
+  \small
   \vskip\abovecaptionskip
   \sbox\@tempboxa{{\bfseries #1.} #2}%
   \ifdim \wd\@tempboxa >\hsize
@@ -873,14 +882,23 @@
 \@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
 \@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
 \@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
+\@ifundefined{extrasngerman}{}{\addto\extrasngerman{\switcht@deutsch}}%
 }{\switcht@@therlang}%
+\providecommand{\keywords}[1]{\par\addvspace\baselineskip
+\noindent\keywordname\enspace\ignorespaces#1}%
 }
 \def\homedir{\~{ }}
 
 \def\subtitle#1{\gdef\@subtitle{#1}}
 \clearheadinfo
-
+%
+%%% to avoid hyperref warnings
+\providecommand*{\toclevel@author}{999}
+%%% to make title-entry parent of section-entries
+\providecommand*{\toclevel@title}{0}
+%
 \renewcommand\maketitle{\newpage
+\phantomsection
   \refstepcounter{chapter}%
   \stepcounter{section}%
   \setcounter{section}{0}%
@@ -909,8 +927,8 @@
     \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
     \instindent=\hsize
     \advance\instindent by-\headlineindent
-%    \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
-%       \addcontentsline{toc}{title}{\the\toctitle}\fi
+    \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
+       \addcontentsline{toc}{title}{\the\toctitle}\fi
     \if@runhead
        \if!\the\titlerunning!\else
          \edef\@title{\the\titlerunning}%
@@ -934,7 +952,8 @@
       \protected@xdef\scratch{\the\tocauthor}%
       \protected@xdef\toc@uthor{\scratch}%
     \fi
-%    \addcontentsline{toc}{author}{\toc@uthor}%
+    \addtocontents{toc}{\noexpand\protect\noexpand\authcount{\the\c@auco}}%
+    \addcontentsline{toc}{author}{\toc@uthor}%
     \if@runhead
        \if!\the\authorrunning!
          \value{@inst}=\value{@auth}%
@@ -1038,9 +1057,9 @@
 \def\@spothm#1[#2]#3#4#5{%
   \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
   {\expandafter\@ifdefinable\csname #1\endcsname
-  {\global\@namedef{the#1}{\@nameuse{the#2}}%
+  {\newaliascnt{#1}{#2}%
   \expandafter\xdef\csname #1name\endcsname{#3}%
-  \global\@namedef{#1}{\@spthm{#2}{\csname #1name\endcsname}{#4}{#5}}%
+  \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
   \global\@namedef{end#1}{\@endtheorem}}}}
 
 \def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@

--- a/thys/Paper/document/root.bib	Mon May 09 15:01:31 2016 +0100
+++ b/thys/Paper/document/root.bib	Wed May 11 12:20:16 2016 +0100
@@ -1,3 +1,14 @@
+
+
+
+@TechReport{CrashCourse2014,
+  author =       {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen},
+  title =        {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular 
+                  {E}xpressions as {T}ypes},
+  institution =  {University of Copenhagen},
+  year =         {2014},
+  annote =       {draft report}
+}
 
 @inproceedings{Sulzmann2014,
   author    = {M.~Sulzmann and K.~Lu},

Binary file thys/paper.pdf has changed