--- a/thys/Paper/Paper.thy	Fri May 20 10:22:12 2016 +0100
+++ b/thys/Paper/Paper.thy	Fri May 20 10:26:40 2016 +0100
@@ -789,7 +789,7 @@
 
   \noindent In (2) we further know by Thm.~\ref{posixdeterm} that the
   value returned by the lexer must be unique.   A simple corollary 
-  of our two theorems yis:
+  of our two theorems is:
 
   \begin{corollary}\mbox{}\smallskip\\\label{lexercorrect}
   \begin{tabular}{ll}