--- a/thys/Paper/Paper.thy	Sat Apr 09 09:51:00 2016 +0100
+++ b/thys/Paper/Paper.thy	Wed Apr 13 12:26:16 2016 +0100
@@ -1129,9 +1129,9 @@
   Nipkow \cite{Nipkow98}. This lexer also splits up strings into longest
   initial substrings, but Nipkow's algorithm is not completely
   computational. The algorithm by Sulzmann and Lu, in contrast, can be
-  implemented with easy in any functional language. A bespoke lexer for the
+  implemented with ease in any functional language. A bespoke lexer for the
   Imp-language is formalised in Coq as part of the Software Foundations book
-  by Pierce et al\cite{Pierce2015}. The disadvantage of such bespoke lexers is that they
+  by Pierce et al \cite{Pierce2015}. The disadvantage of such bespoke lexers is that they
   do not generalise easily to more advanced features.
   Our formalisation is available from
   \url{http://www.inf.kcl.ac.uk/staff/urbanc/lex}.\medskip