diff -r 734341a79028 -r 2ccf3086142b Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Oct 05 08:43:49 2010 +0100
+++ b/Paper/Paper.thy	Tue Oct 05 21:48:31 2010 +0100
@@ -88,8 +88,10 @@
   type-variables.  While it is possible to implement this kind of more general
   binders by iterating single binders, this leads to a rather clumsy
   formalisation of W. The need of iterating single binders is also one reason
-  why Nominal Isabelle and similar theorem provers that only provide
-  mechanisms for binding single variables have not fared extremely well with the
+  why Nominal Isabelle 
+  % and similar theorem provers that only provide
+  %mechanisms for binding single variables 
+  has not fared extremely well with the
   more advanced tasks in the POPLmark challenge \cite{challenge05}, because
   also there one would like to bind multiple variables at once. 
 
@@ -202,7 +204,7 @@
   \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}cl}
   @{text trm} & @{text "::="}  & @{text "\<dots>"} 
               & @{text "|"}  @{text "\<LET>  as::assn  s::trm"}\hspace{2mm} 
-                                 \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
+                                 \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\%%%[1mm]
   @{text assn} & @{text "::="} & @{text "\<ANIL>"}
                &  @{text "|"}  @{text "\<ACONS>  name  trm  assn"}
   \end{tabular}
@@ -277,7 +279,7 @@
   construction we perform in Isabelle/HOL can be illustrated by the following picture:
   %
   \begin{center}
-  \begin{tikzpicture}[scale=0.9]
+  \begin{tikzpicture}[scale=0.89]
   %\draw[step=2mm] (-4,-1) grid (4,1);
   
   \draw[very thick] (0.7,0.4) circle (4.25mm);
@@ -506,30 +508,30 @@
   @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
   \end{property}
 
-  While often the support of an object can be relatively easily 
-  described, for example for atoms, products, lists, function applications, 
-  booleans and permutations as follows
+  %While often the support of an object can be relatively easily 
+  %described, for example for atoms, products, lists, function applications, 
+  %booleans and permutations as follows
+  %%
+  %\begin{center}
+  %\begin{tabular}{c@ {\hspace{10mm}}c}
+  %\begin{tabular}{rcl}
+  %@{term "supp a"} & $=$ & @{term "{a}"}\\
+  %@{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
+  %@{term "supp []"} & $=$ & @{term "{}"}\\
+  %@{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\
+  %\end{tabular}
+  %&
+  %\begin{tabular}{rcl}
+  %@{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
+  %@{term "supp b"} & $=$ & @{term "{}"}\\
+  %@{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
+  %\end{tabular}
+  %\end{tabular}
+  %\end{center}
   %
-  \begin{center}
-  \begin{tabular}{c@ {\hspace{10mm}}c}
-  \begin{tabular}{rcl}
-  @{term "supp a"} & $=$ & @{term "{a}"}\\
-  @{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
-  @{term "supp []"} & $=$ & @{term "{}"}\\
-  @{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\
-  \end{tabular}
-  &
-  \begin{tabular}{rcl}
-  @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
-  @{term "supp b"} & $=$ & @{term "{}"}\\
-  @{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
-  \end{tabular}
-  \end{tabular}
-  \end{center}
-  
-  \noindent 
-  in some cases it can be difficult to characterise the support precisely, and
-  only an approximation can be established (as for functions above). 
+  %\noindent 
+  %in some cases it can be difficult to characterise the support precisely, and
+  %only an approximation can be established (as for functions above). 
 
   %Reasoning about
   %such approximations can be simplified with the notion \emph{supports}, defined 
@@ -576,10 +578,14 @@
   %\begin{center}
   %@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
   %\end{center}
-
-  Using support and freshness, the nominal logic work provides us with general means for renaming 
-  binders. While in the older version of Nominal Isabelle, we used extensively 
-  Property~\ref{swapfreshfresh} to rename single binders, this property 
+  %
+  %Using freshness, the nominal logic work provides us with general means for renaming 
+  %binders. 
+  %
+  \noindent
+  While in the older version of Nominal Isabelle, we used extensively 
+  %Property~\ref{swapfreshfresh}
+  this property to rename single binders, it %%this property 
   proved too unwieldy for dealing with multiple binders. For such binders the 
   following generalisations turned out to be easier to use.
 
@@ -880,7 +886,7 @@
   \mbox{\begin{tabular}{@ {}p{2.5cm}l}
   type \mbox{declaration part} &
   $\begin{cases}
-  \mbox{\begin{tabular}{l}
+  \mbox{\small\begin{tabular}{l}
   \isacommand{nominal\_datatype} @{text "ty\<AL>\<^isub>1 = \<dots>"}\\
   \isacommand{and} @{text "ty\<AL>\<^isub>2 = \<dots>"}\\
   \raisebox{2mm}{$\ldots$}\\[-2mm] 
@@ -889,7 +895,7 @@
   \end{cases}$\\
   binding \mbox{function part} &
   $\begin{cases}
-  \mbox{\begin{tabular}{l}
+  \mbox{\small\begin{tabular}{l}
   \isacommand{binder} @{text "bn\<AL>\<^isub>1"} \isacommand{and} \ldots \isacommand{and} @{text "bn\<AL>\<^isub>m"}\\
   \isacommand{where}\\
   \raisebox{2mm}{$\ldots$}\\[-2mm]
@@ -979,8 +985,7 @@
   single name is bound, and type-schemes, where a finite set of names is
   bound:
 
-
-  \begin{center}
+  \begin{center}\small
   \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
   \begin{tabular}{@ {}l}
   \isacommand{nominal\_datatype} @{text lam} $=$\\
@@ -1020,7 +1025,7 @@
   tuple patterns might be specified as:
   %
   \begin{equation}\label{letpat}
-  \mbox{%
+  \mbox{\small%
   \begin{tabular}{l}
   \isacommand{nominal\_datatype} @{text trm} =\\
   \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
@@ -1063,7 +1068,7 @@
   specification:
   %
   \begin{equation}\label{letrecs}
-  \mbox{%
+  \mbox{\small%
   \begin{tabular}{@ {}l@ {}}
   \isacommand{nominal\_datatype}~@{text "trm ="}\ldots\\
   \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 
@@ -1132,7 +1137,7 @@
   clause, written \isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "labels"}. In case
   of the lambda-terms, the completion produces
 
-  \begin{center}
+  \begin{center}\small
   \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
   \isacommand{nominal\_datatype} @{text lam} =\\
   \hspace{5mm}\phantom{$\mid$}~@{text "Var x::name"}
@@ -1172,13 +1177,7 @@
   But for the purpose of this paper, we use the superscript @{text "_\<^sup>\<alpha>"} to indicate 
   that a notion is given for $\alpha$-equivalence classes and leave it out 
   for the corresponding notion given on the ``raw'' level. So for example 
-  we have
-  
-  \begin{center}
-  @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
-  \end{center}
-  
-  \noindent
+  we have @{text "ty\<^sup>\<alpha> \<mapsto> ty"} and @{text "C\<^sup>\<alpha> \<mapsto> C"}
   where @{term ty} is the type used in the quotient construction for 
   @{text "ty\<^sup>\<alpha>"} and @{text "C"} is the term-constructor on the ``raw'' type @{text "ty"}. 
 
@@ -2233,12 +2232,13 @@
 
   \medskip
   \noindent
-  {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
-  many discussions about Nominal Isabelle. We also thank Peter Sewell for 
+  {\bf Acknowledgements:} %We are very grateful to Andrew Pitts for  
+  %many discussions about Nominal Isabelle. 
+  We thank Peter Sewell for 
   making the informal notes \cite{SewellBestiary} available to us and 
   also for patiently explaining some of the finer points of the work on the Ott-tool.
-  Stephanie Weirich suggested to separate the subgrammars
-  of kinds and types in our Core-Haskell example.  
+  %Stephanie Weirich suggested to separate the subgrammars
+  %of kinds and types in our Core-Haskell example.  
 
 *}