--- a/Paper/Paper.thy	Fri Oct 29 15:37:24 2010 +0100
+++ b/Paper/Paper.thy	Fri Nov 05 15:21:10 2010 +0000
@@ -524,11 +524,11 @@
   swapping two fresh atoms, say @{text a} and @{text b}, leaves 
   @{text x} unchanged, namely if @{text "a \<FRESH> x"} and @{text "b \<FRESH> x"}
   then @{term "(a \<rightleftharpoons> b) \<bullet> x"}.
-
+  %
   %\begin{myproperty}\label{swapfreshfresh}
   %@{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
   %\end{myproperty}
-
+  %
   %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
@@ -553,7 +553,7 @@
   %\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 
   %as follows:
@@ -603,7 +603,7 @@
   %Using freshness, the nominal logic work provides us with general means for renaming 
   %binders. 
   %
-  \noindent
+  %\noindent
   While in the older version of Nominal Isabelle, we used extensively 
   %Property~\ref{swapfreshfresh}
   this property to rename single binders, it %%this property