
diff -r 0b94800eb616 -r 0f9fdb62d28a thys/Paper/Paper.thy
--- 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}




