# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1463736400 -3600
# Node ID 0f9fdb62d28ae140d5495a53f7d68f962e2723d2
# Parent  0b94800eb61643b693e1aad705353d8a24ff9104
typo

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}