# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1464948430 -3600
# Node ID 1fd7388360b6f097c11a049d5a5a6d6132c0e062
# Parent  f101eac348f827d3a7fedc33b1e0e2197f12914f
typos

diff -r f101eac348f8 -r 1fd7388360b6 thys/Lexer.thy
--- a/thys/Lexer.thy	Tue May 24 15:13:41 2016 +0100
+++ b/thys/Lexer.thy	Fri Jun 03 11:07:10 2016 +0100
@@ -620,7 +620,6 @@
 
 lemma lexer_correct_None:
   shows "s \<notin> L r \<longleftrightarrow> lexer r s = None"
-using assms
 apply(induct s arbitrary: r)
 apply(simp add: nullable_correctness)
 apply(drule_tac x="der a r" in meta_spec)
@@ -629,7 +628,6 @@
 
 lemma lexer_correct_Some:
   shows "s \<in> L r \<longleftrightarrow> (\<exists>v. lexer r s = Some(v) \<and> s \<in> r \<rightarrow> v)"
-using assms
 apply(induct s arbitrary: r)
 apply(auto simp add: Posix_mkeps nullable_correctness)[1]
 apply(drule_tac x="der a r" in meta_spec)
diff -r f101eac348f8 -r 1fd7388360b6 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue May 24 15:13:41 2016 +0100
+++ b/thys/Paper/Paper.thy	Fri Jun 03 11:07:10 2016 +0100
@@ -791,7 +791,7 @@
   value returned by the lexer must be unique.   A simple corollary 
   of our two theorems is:
 
-  \begin{corollary}\mbox{}\smallskip\\\label{lexercorrect}
+  \begin{corollary}\mbox{}\smallskip\\\label{lexercorrectcor}
   \begin{tabular}{ll}
   (1) & @{thm (lhs) lexer_correctness(2)} if and only if @{thm (rhs) lexer_correctness(2)}\\ 
   (2) & @{thm (lhs) lexer_correctness(1)} if and only if @{thm (rhs) lexer_correctness(1)}\\
diff -r f101eac348f8 -r 1fd7388360b6 thys/Simplifying.thy
--- a/thys/Simplifying.thy	Tue May 24 15:13:41 2016 +0100
+++ b/thys/Simplifying.thy	Fri Jun 03 11:07:10 2016 +0100
@@ -75,7 +75,6 @@
 
 lemma L_fst_simp:
   shows "L(r) = L(fst (simp r))"
-using assms
 by (induct r) (auto)
 
 lemma Posix_simp:
diff -r f101eac348f8 -r 1fd7388360b6 thys/paper.pdf
Binary file thys/paper.pdf has changed