--- a/Paper/Paper.thy	Fri Mar 19 15:43:59 2010 +0100
+++ b/Paper/Paper.thy	Fri Mar 19 17:20:25 2010 +0100
@@ -220,8 +220,30 @@
   can perform in HOL is illustrated by the following picture:
  
   \begin{center}
-  figure
-  %\begin{pspicture}(0.5,0.0)(8,2.5)
+  \begin{tikzpicture}
+  %\draw[step=2mm] (-4,-1) grid (4,1);
+  
+  \draw[very thick] (0.7,0.4) circle (4.25mm);
+  \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);
+  \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);
+  
+  \draw (-2.0, 0.845) --  (0.7,0.845);
+  \draw (-2.0,-0.045)  -- (0.7,-0.045);
+
+  \draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
+  \draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
+  \draw (1.8, 0.48) node[right=-0.1mm]
+    {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+  \draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+  \draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
+  
+  \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
+  \draw (-0.95, 0.3) node[above=0mm] {isomorphism};
+
+  %\rput(3.7,1.75){isomorphism}
+  \end{tikzpicture}
+
+  %%\begin{pspicture}(0.5,0.0)(8,2.5)
   %%\showgrid
   %\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5)
   %\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6}
@@ -255,9 +277,9 @@
   inspired by earlier work of Pitts \cite{}. By means of automatic
   proofs, we establish a reasoning infrastructure for alpha-equated
   terms, including properties about support, freshness and equality
-  conditions for alpha-equated terms. We will also derive for these
-  terms a strong induction principle that has the variable convention
-  already built in.
+  conditions for alpha-equated terms. We re also able to derive, at the moment 
+  only manually, for these terms a strong induction principle that 
+  has the variable convention already built in.
 *}
 
 section {* A Short Review of the Nominal Logic Work *}