--- a/Paper/Paper.thy	Wed Mar 17 20:42:42 2010 +0100
+++ b/Paper/Paper.thy	Thu Mar 18 00:17:21 2010 +0100
@@ -2,6 +2,13 @@
 theory Paper
 imports "../Nominal/Test"
 begin
+
+notation (latex output)
+  swap ("'(_ _')" [1000, 1000] 1000) and
+  fresh ("_ # _" [51, 51] 50) and
+  supp ("supp _" [78] 73) and
+  uminus ("-_" [78] 73) and
+  If  ("if _ then _ else _" 10)
 (*>*)
 
 section {* Introduction *}
@@ -22,16 +29,69 @@
   involving general bindings are alpha-equivelent.
 *}
 
-section {* A Brief Overview about the Nominal Logic Work *}
+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}. The 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.
+
+  Permutations are bijective functions from atoms to atoms that are 
+  the identity everywhere except on a finite number of atoms. There is a 
+  two-place permutation operation written
+
+  @{text [display,indent=5] "_ \<bullet> _  ::  (\<alpha> \<times> \<alpha>) list \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
+
+  \noindent 
+  with a generic type in which @{text "\<alpha>"} stands for the type of atoms 
+  and @{text "\<beta>"} for the type of the objects on which the permutation 
+  acts. In Nominal Isabelle the identity permutation is written as @{term "0::perm"},
+  the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}} 
+  and the inverse permutation @{term p} as @{text "- p"}. The permutation
+  operation is defined for products, lists, sets, functions, booleans etc 
+  (see \cite{HuffmanUrban10}).
+
+  The most original aspect of the nominal logic work of Pitts et al is a general
+  definition for ``the set of free variables of an object @{text "x"}''.  This
+  definition is general in the sense that it applies not only to lambda-terms,
+  but also to lists, products, sets and even functions. The definition depends
+  only on the permutation operation and on the notion of equality defined for
+  the type of @{text x}, namely:
+
+  @{thm [display,indent=5] supp_def[no_vars, THEN eq_reflection]}
+
+  \noindent
+  There is also the derived notion for when an atom @{text a} is \emph{fresh}
+  for an @{text x}, defined as
+  
+  @{thm [display,indent=5] fresh_def[no_vars]}
+
+  \noindent
+  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. For the proof we use the following lemma 
+  about swappings applied to an @{text x}:
+
+*}
+
 
 section {* Abstractions *}
 
 section {* Alpha-Equivalence and Free Variables *}
 
+section {* Examples *}
 
+section {* Conclusion *}
 
 text {*
-  Acknowledgements: We thank Andrew Pitts for the many discussions
+
+  \noindent
+  {\bf Acknowledgements:} We thank Andrew Pitts for the many discussions
   about the topic. We thank Peter Sewell for making [] available 
   to us and explaining some of the finer points of the OTT tool.