--- a/Paper/Paper.thy	Mon Oct 04 12:39:57 2010 +0100
+++ b/Paper/Paper.thy	Tue Oct 05 07:30:37 2010 +0100
@@ -60,13 +60,8 @@
 text {*
 
   So far, Nominal Isabelle provided a mechanism for constructing
-  $\alpha$-equated terms, for example lambda-terms
-  %
-  \begin{center}
-  @{text "t ::= x | t t | \<lambda>x. t"}
-  \end{center}
-  %
-  \noindent
+  $\alpha$-equated terms, for example lambda-terms,
+  @{text "t ::= x | t t | \<lambda>x. t"},
   where free and bound variables have names.  For such $\alpha$-equated terms,
   Nominal Isabelle derives automatically a reasoning infrastructure that has
   been used successfully in formalisations of an equivalence checking
@@ -83,7 +78,7 @@
   %
   \begin{equation}\label{tysch}
   \begin{array}{l}
-  @{text "T ::= x | T \<rightarrow> T"}\hspace{5mm}
+  @{text "T ::= x | T \<rightarrow> T"}\hspace{9mm}
   @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
   \end{array}
   \end{equation}
@@ -239,13 +234,7 @@
 
   However, we will not be able to cope with all specifications that are
   allowed by Ott. One reason is that Ott lets the user specify ``empty'' 
-  types like
-  %
-  \begin{center}
-  @{text "t ::= t t | \<lambda>x. t"}
-  \end{center}
-  %
-  \noindent
+  types like @{text "t ::= t t | \<lambda>x. t"}
   where no clause for variables is given. Arguably, such specifications make
   some sense in the context of Coq's type theory (which Ott supports), but not
   at all in a HOL-based environment where every datatype must have a non-empty
@@ -288,7 +277,7 @@
   construction we perform in Isabelle/HOL can be illustrated by the following picture:
   %
   \begin{center}
-  \begin{tikzpicture}
+  \begin{tikzpicture}[scale=0.9]
   %\draw[step=2mm] (-4,-1) grid (4,1);
   
   \draw[very thick] (0.7,0.4) circle (4.25mm);