--- 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)

--- 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)}\\

--- 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:

Binary file thys/paper.pdf has changed