--- a/Quotient-Paper-jv/Paper.thy	Fri Feb 17 15:23:38 2012 +0100
+++ b/Quotient-Paper-jv/Paper.thy	Wed Feb 22 12:10:17 2012 +0000
@@ -146,7 +146,7 @@
 %%% I wouldn't change it.
 
   \begin{center}
-  \mbox{}\hspace{20mm}\begin{tikzpicture}[scale=0.9]
+  \mbox{}\hspace{20mm}\begin{tikzpicture}[scale=1.1]
   %%\draw[step=2mm] (-4,-1) grid (4,1);
 
   \draw[very thick] (0.7,0.3) circle (4.85mm);
@@ -222,8 +222,10 @@
   flattens lists of lists, defined as follows
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm}
-  @{thm concat.simps(2)[THEN eq_reflection]}
+  \begin{tabular}{@ {}l}
+  @{thm concat.simps(1)[THEN eq_reflection]}\\
+  @{thm concat.simps(2)[THEN eq_reflection, where x1="x" and xs1="xs"]}
+  \end{tabular}
   \end{isabelle}
 
   \noindent
@@ -233,8 +235,10 @@
   builds finite unions of finite sets:
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{thm concat_empty_fset[THEN eq_reflection]}\hspace{10mm}
-  @{thm concat_insert_fset[THEN eq_reflection]}
+  \begin{tabular}{@ {}l}
+  @{thm concat_empty_fset[THEN eq_reflection]}\\
+  @{thm concat_insert_fset[THEN eq_reflection, where x1="x" and S1="S"]}
+  \end{tabular}
   \end{isabelle}
 
   \noindent