diff -r 6b0a1976f89a -r 072a701bb153 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Fri May 06 11:33:21 2016 +0100
+++ b/thys/Paper/Paper.thy	Sun May 08 09:32:50 2016 +0100
@@ -84,7 +84,8 @@
 just consist of inductive datatypes and simple recursive functions. A
 completely formalised correctness proof of this matcher in for example HOL4
 has been mentioned by Owens and Slind~\cite{Owens2008}. Another one in Isabelle/HOL is part
-of the work by Krauss and Nipkow \cite{Krauss2011}.
+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.
@@ -102,20 +103,10 @@
 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. Beginning with our
-observations that, without evidence that it is transitive, it cannot be
-called an ``order relation'', and that the relation is called a ``total
-order'' despite being evidently not total\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.}, we
-identify problems with this approach (of which some of the proofs are not
+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{arg} we
+identify 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
@@ -126,6 +117,18 @@
 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
@@ -902,7 +905,7 @@
 
 *}
 
-section {* The Correctness Argument by Sulzmmann and Lu *}
+section {* The Correctness Argument by Sulzmmann and Lu\label{argu} *}
 
 text {*
 %  \newcommand{\greedy}{\succcurlyeq_{gr}}