# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1643504606 0
# Node ID 8bbe2468fedcca78a1147cecc10ec70ee4434156
# Parent  46e5566ad4ba2860e45f0cb2709b44277a20c961
updated

diff -r 46e5566ad4ba -r 8bbe2468fedc thys2/Paper/document/root.tex
--- a/thys2/Paper/document/root.tex	Sat Jan 29 23:53:21 2022 +0000
+++ b/thys2/Paper/document/root.tex	Sun Jan 30 01:03:26 2022 +0000
@@ -66,7 +66,7 @@
   of the regular expression.  The purpose of the bitcodes in Sulzmann
   and Lu's algorithm is to generate POSIX values incrementally while
   derivatives are calculated. However they also help with designing
-  `aggressive' simplification methods that keep the size of
+  `aggressive' simplification functions that keep the size of
   derivatives small. Without simplification derivatives can grow
   exponentially resulting in an extremely slow lexing algorithm.  In this
   paper we describe a variant of Sulzmann and Lu's algorithm: Our
@@ -75,8 +75,9 @@
   prove in Isabelle/HOL that our program is correct and generates
   unique POSIX values; we also \textit{(ii)} establish a polynomial
   bound for the size of the derivatives. The size can be seen as a
-  proxy measure for the effeciency of the lexing algorithm---that means
-  our algorithm does not suffer from the exponential blowup.
+  proxy measure for the efficiency of the lexing algorithm---that means
+  because of the polynomial bound our algorithm does not suffer from
+  the exponential blowup in earlier works.
   
   % Brzozowski introduced the notion of derivatives for regular
   % expressions. They can be used for a very simple regular expression
diff -r 46e5566ad4ba -r 8bbe2468fedc thys2/paper.pdf
Binary file thys2/paper.pdf has changed