--- a/thys2/Paper/Paper.thy	Sat Jan 29 16:43:51 2022 +0000
+++ b/thys2/Paper/Paper.thy	Sat Jan 29 23:53:21 2022 +0000
@@ -34,24 +34,31 @@
 
 text {*
 
-Brzozowski \cite{Brzozowski1964} introduced the notion of the {\em
-derivative} @{term "der c r"} of a regular expression \<open>r\<close> w.r.t.\
-a character~\<open>c\<close>, and showed that it gave a simple solution to the
-problem of matching a string @{term s} with a regular expression @{term
-r}: if the derivative of @{term r} w.r.t.\ (in succession) all the
-characters of the string matches the empty string, then @{term r}
-matches @{term s} (and {\em vice versa}). The derivative has the
-property (which may almost be regarded as its specification) that, for
-every string @{term s} and regular expression @{term r} and character
-@{term c}, one has @{term "cs \<in> L(r)"} if and only if \mbox{@{term "s \<in> L(der c r)"}}. 
-The beauty of Brzozowski's derivatives is that
-they are neatly expressible in any functional language, and easily
-definable and reasoned about in theorem provers---the definitions just
-consist of inductive datatypes and simple recursive functions. A
-mechanised correctness proof of Brzozowski's 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}.
-And another one in Coq is given by Coquand and Siles \cite{Coquand2012}.
+In the last fifteen or so years, Brzozowski's derivatives of regular
+expressions have sparked quite a bit of interest in the functional
+programming and theorem prover communities.  The beauty of
+Brzozowski's derivatives \cite{Brzozowski1964} is that they are neatly
+expressible in any functional language, and easily definable and
+reasoned about in theorem provers---the definitions just consist of
+inductive datatypes and simple recursive functions. A mechanised
+correctness proof of Brzozowski's 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}.  And another one in Coq is given by Coquand and
+Siles \cite{Coquand2012}.
+
+
+The notion of derivatives
+\cite{Brzozowski1964}, written @{term "der c r"}, of a regular
+expression give a simple solution to the problem of matching a string
+@{term s} with a regular expression @{term r}: if the derivative of
+@{term r} w.r.t.\ (in succession) all the characters of the string
+matches the empty string, then @{term r} matches @{term s} (and {\em
+vice versa}). The derivative has the property (which may almost be
+regarded as its specification) that, for every string @{term s} and
+regular expression @{term r} and character @{term c}, one has @{term
+"cs \<in> L(r)"} if and only if \mbox{@{term "s \<in> L(der c r)"}}.
+
 
 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
@@ -158,6 +165,8 @@
 section {* Simplification *}
 
 text {*
+     Sulzmann \& Lu apply simplification via a fixpoint operation; also does not use erase to filter out duplicates.
+
    not direct correspondence with PDERs, because of example
    problem with retrieve