# HG changeset patch # User Christian Urban # Date 1462965616 -3600 # Node ID f1d800062d4faaddd75fb7f556bdebd829491199 # Parent fc22ca36325c54aa66754448056101f8d820f3b4 updated diff -r fc22ca36325c -r f1d800062d4f thys/Paper/Paper.thy --- 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 "\\<^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 "\\<^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>\"} 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>\"} 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 "\\<^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 "\\<^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} diff -r fc22ca36325c -r f1d800062d4f thys/Paper/document/llncs.cls --- 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@ diff -r fc22ca36325c -r f1d800062d4f thys/Paper/document/root.bib --- 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}, diff -r fc22ca36325c -r f1d800062d4f thys/paper.pdf Binary file thys/paper.pdf has changed