diff -r 2e70c1b06ac0 -r 685bff2890d5 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue May 17 10:53:34 2016 +0100
+++ b/thys/Paper/Paper.thy	Tue May 17 11:16:56 2016 +0100
@@ -624,7 +624,7 @@
   \mbox{@{term "s \<in> r \<rightarrow> v"}}, relating strings, regular expressions and
   values.
   %
-  \begin{center}\small
+  \begin{center}
   \begin{tabular}{c}
   @{thm[mode=Axiom] Posix.intros(1)}@{text "P"}@{term "ONE"} \qquad
   @{thm[mode=Axiom] Posix.intros(2)}@{text "P"}@{term "c"}\medskip\\
@@ -868,8 +868,7 @@
   The rectification functions can be (slightly clumsily) implemented  in
   Isabelle/HOL as follows using some auxiliary functions:
 
-  \begin{center}\small
-  \begin{tabular}{cc}
+  \begin{center}
   \begin{tabular}{lcl}
   @{thm (lhs) F_RIGHT.simps(1)} & $\dn$ & @{text "Right (f v)"}\\
   @{thm (lhs) F_LEFT.simps(1)} & $\dn$ & @{text "Left (f v)"}\\
@@ -879,9 +878,9 @@
   
   @{thm (lhs) F_SEQ1.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 ()) (f\<^sub>2 v)"}\\
   @{thm (lhs) F_SEQ2.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v) (f\<^sub>2 ())"}\\
-  @{thm (lhs) F_SEQ.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"}%\bigskip\\
+  @{thm (lhs) F_SEQ.simps(1)} & $\dn$ & @{text "Seq (f\<^sub>1 v\<^sub>1) (f\<^sub>2 v\<^sub>2)"}\medskip\\
   \end{tabular}
-  &
+
   \begin{tabular}{lcl}
   @{term "simp_ALT (ZERO, DUMMY) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>2, F_RIGHT f\<^sub>2)"}\\
   @{term "simp_ALT (r\<^sub>1, f\<^sub>1) (ZERO, DUMMY)"} & $\dn$ & @{term "(r\<^sub>1, F_LEFT f\<^sub>1)"}\\
@@ -890,7 +889,6 @@
   @{term "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2)"} & $\dn$ & @{term "(r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"}\\
   @{term "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2)"} & $\dn$ & @{term "(SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"}\\
   \end{tabular}
-  \end{tabular}
   \end{center}
 
   \noindent
@@ -960,7 +958,7 @@
   \end{proof}
 
   \noindent We can now prove relatively straightforwardly that the
-  optimised lexer produce the expected result:
+  optimised lexer produces the expected result:
 
   \begin{theorem}
   @{thm slexer_correctness}
@@ -971,27 +969,27 @@
   string is of the form @{term "c # s"}. By induction hypothesis we
   know @{term "slexer r s = lexer r s"} holds for all @{term r} (in
   particular for @{term "r"} being the derivative @{term "der c
-  r"}). Let @{term "r\<^sub>s"} be the simplified derivative regular expression, @{term
+  r"}). Let @{term "r\<^sub>s"} be the simplified derivative regular expression, that is @{term
   "fst (simp (der c r))"}, and @{term "f\<^sub>r"} be the rectification
-  function, @{term "snd (simp (der c r))"}.  We distinguish the cases
+  function, that is @{term "snd (simp (der c r))"}.  We distinguish the cases
   whether (*) @{term "s \<in> L (der c r)"} or not. In the first case we
-  have by Thm~\ref{lexercorrect}(2) a value @{term "v"} so that @{term
+  have by Thm.~\ref{lexercorrect}(2) a value @{term "v"} so that @{term
   "lexer (der c r) s = Some v"} and @{term "s \<in> der c r \<rightarrow> v"} hold.
-  By Lem~\ref{slexeraux}(1) we can also infer from~(*) that @{term "s
-  \<in> L r\<^sub>s"} holds.  Hence we know by Thm~\ref{lexercorrect}(2) that
+  By Lem.~\ref{slexeraux}(1) we can also infer from~(*) that @{term "s
+  \<in> L r\<^sub>s"} holds.  Hence we know by Thm.~\ref{lexercorrect}(2) that
   there exists a @{term "v'"} with @{term "lexer r\<^sub>s s = Some v'"} and
   @{term "s \<in> r\<^sub>s \<rightarrow> v'"}. From the latter we know by
-  Lem~\ref{slexeraux}(2) that @{term "s \<in> der c r \<rightarrow> (f\<^sub>r v')"} holds.
-  By the uniqueness of the POSIX relation (Thm~\ref{posixdeterm}) we
+  Lem.~\ref{slexeraux}(2) that @{term "s \<in> der c r \<rightarrow> (f\<^sub>r v')"} holds.
+  By the uniqueness of the POSIX relation (Thm.~\ref{posixdeterm}) we
   can infer that @{term v} is equal to @{term "f\<^sub>r v'"}---that is the 
   rectification function applied to @{term "v'"}
   produces the original @{term "v"}.  Now the case follows by the
   definitions of @{const lexer} and @{const slexer}.
 
   In the second case where @{term "s \<notin> L (der c r)"} we have that
-  @{term "lexer (der c r) s = None"} by Thm~\ref{lexercorrect}(1).  We
-  also know by Lem~\ref{slexeraux}(1) that @{term "s \<notin> L r\<^sub>s"}. Hence
-  @{term "lexer r\<^sub>s s = None"} by Thm~\ref{lexercorrect}(1) and
+  @{term "lexer (der c r) s = None"} by Thm.~\ref{lexercorrect}(1).  We
+  also know by Lem.~\ref{slexeraux}(1) that @{term "s \<notin> L r\<^sub>s"}. Hence
+  @{term "lexer r\<^sub>s s = None"} by Thm.~\ref{lexercorrect}(1) and
   by IH then also @{term "slexer r\<^sub>s s = None"}. With this we can
   conclude in this case too.\qed   
 
@@ -1012,7 +1010,7 @@
   Their central definition is an ``ordering relation'' defined by the
   rules (slightly adapted to fit our notation):
 
-\begin{center}\small  
+\begin{center}  
 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}	
 @{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) &
 @{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\