--- a/Paper/Paper.thy	Thu Mar 18 15:32:49 2010 +0100
+++ b/Paper/Paper.thy	Thu Mar 18 16:22:10 2010 +0100
@@ -51,19 +51,21 @@
   %\end{pspicture}
   %\end{center}
 
-
+  quotient package \cite{Homeier05}
 *}
 
 section {* A Short Review of the Nominal Logic Work *}
 
 text {*
   At its core, Nominal Isabelle is based on the nominal logic work by Pitts
-  \cite{Pitts03}. Two central notions in this work are sorted atoms and
-  permutations of atoms. The sorted atoms represent different
-  kinds of variables, such as term- and type-variables in Core-Haskell, and it
-  is assumed that there is an infinite supply of atoms for each sort. 
-  However, in order to simplify the description of our work, we shall
-  assume in this paper that there is only a single sort of atoms.
+  \cite{Pitts03}. The implementation of this work are described in
+  \cite{HuffmanUrban10}, which we review here briefly to aid the description
+  of what follows in the next sections. Two central notions in the nominal
+  logic work are sorted atoms and permutations of atoms. The sorted atoms
+  represent different kinds of variables, such as term- and type-variables in
+  Core-Haskell, and it is assumed that there is an infinite supply of atoms
+  for each sort. However, in order to simplify the description of our work, we
+  shall assume in this paper that there is only a single sort of atoms.
 
   Permutations are bijective functions from atoms to atoms that are 
   the identity everywhere except on a finite number of atoms. There is a 
@@ -96,38 +98,55 @@
   @{thm[display,indent=5] fresh_def[no_vars]}
 
   \noindent
-  We also use for sets of atoms the abbreviation @{thm fresh_star_def[no_vars]}.
+  We also use for sets of atoms the abbreviation 
+  @{thm (lhs) fresh_star_def[no_vars]} defined as 
+  @{thm (rhs) fresh_star_def[no_vars]}.
   A striking consequence of these definitions is that we can prove
   without knowing anything about the structure of @{term x} that
   swapping two fresh atoms, say @{text a} and @{text b}, leave 
   @{text x} unchanged. 
 
-  \begin{Property}
+  \begin{property}
   @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
-  \end{Property}
+  \end{property}
 
-  \begin{Property}
+  \noindent
+  For a proof see \cite{HuffmanUrban10}.
+
+  \begin{property}
   @{thm[mode=IfThen] at_set_avoiding[no_vars]}
-  \end{Property}
+  \end{property}
 
 *}
 
 
 section {* Abstractions *}
 
+text {*
+  General notion of alpha-equivalence (depends on a free-variable
+  function and a relation).
+*}
+
 section {* Alpha-Equivalence and Free Variables *}
 
 section {* Examples *}
 
+section {* Adequacy *}
+
+section {* Related Work *}
+
 section {* Conclusion *}
 
 text {*
 
+  TODO: function definitions:
+  \medskip
+
   \noindent
   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for the 
   many discussions about Nominal Isabelle. We thank Peter Sewell for 
   making the informal notes \cite{SewellBestiary} available to us and 
-  also explaining some of the finer points of the OTT-tool.
+  also for explaining some of the finer points of the OTT-tool.
 
 
 *}