Mercurial Mercurial > hg > lexing / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Paper/Paper.thy
changeset 187 0f9fdb62d28a
parent 186 0b94800eb616
child 189 419041034e35
equal deleted inserted replaced
186:0b94800eb616 187:0f9fdb62d28a 
   787   By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{Posix2}.\qed  
   787   By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{Posix2}.\qed  
   788   \end{proof}
 
   788   \end{proof}
 
   789 
   789 
   790   \noindent In (2) we further know by Thm.~\ref{posixdeterm} that the
 
   790   \noindent In (2) we further know by Thm.~\ref{posixdeterm} that the
 
   791   value returned by the lexer must be unique.   A simple corollary 
   791   value returned by the lexer must be unique.   A simple corollary 
   792   of our two theorems yis:
 
   792   of our two theorems is:
 
   793 
   793 
   794   \begin{corollary}\mbox{}\smallskip\\\label{lexercorrect}
 
   794   \begin{corollary}\mbox{}\smallskip\\\label{lexercorrect}
 
   795   \begin{tabular}{ll}
 
   795   \begin{tabular}{ll}
 
   796   (1) & @{thm (lhs) lexer_correctness(2)} if and only if @{thm (rhs) lexer_correctness(2)}\\ 
   796   (1) & @{thm (lhs) lexer_correctness(2)} if and only if @{thm (rhs) lexer_correctness(2)}\\ 
   797   (2) & @{thm (lhs) lexer_correctness(1)} if and only if @{thm (rhs) lexer_correctness(1)}\\
 
   797   (2) & @{thm (lhs) lexer_correctness(1)} if and only if @{thm (rhs) lexer_correctness(1)}\\
lexing