--- a/Paper/Paper.thy	Thu Mar 18 10:15:57 2010 +0100
+++ b/Paper/Paper.thy	Thu Mar 18 11:33:37 2010 +0100
@@ -1,11 +1,12 @@
 (*<*)
 theory Paper
-imports "../Nominal/Test"
+imports "../Nominal/Test" "LaTeXsugar"
 begin
 
 notation (latex output)
   swap ("'(_ _')" [1000, 1000] 1000) and
   fresh ("_ # _" [51, 51] 50) and
+  fresh_star ("_ #* _" [51, 51] 50) and
   supp ("supp _" [78] 73) and
   uminus ("-_" [78] 73) and
   If  ("if _ then _ else _" 10)
@@ -20,20 +21,44 @@
   where ...
 
   The difficulty can be appreciated by considering that the
-  definition given by Leroy in [] is incorrect (it omits a
+  definition given by Leroy in \cite{Leroy92} is incorrect (it omits a
   side-condition).
 
   Examples: type-schemes, Spi-calculus
 
   Contributions:  We provide definitions for when terms
   involving general bindings are alpha-equivelent.
+
+  %\begin{center}
+  %\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}
+  %\psframe[linewidth=0.4mm,framearc=0.2,dimen=middle](1.1,2.1)(2.3,0.9)
+  
+  %\pcline[linewidth=0.4mm]{->}(2.6,1.5)(4.8,1.5)
+  
+  %\pcline[linewidth=0.2mm](2.2,2.1)(6,2.1)
+  %\pcline[linewidth=0.2mm](2.2,0.9)(6,0.9)
+
+  %\rput(7.3,2.2){$\mathtt{phi}$}
+  %\rput(6,1.5){$\lama$}
+  %\rput[l](7.6,2.05){\begin{tabular}{l}existing\\[-1.6mm]type\end{tabular}}
+  %\rput[r](1.2,1.5){\begin{tabular}{l}new\\[-1.6mm]type\end{tabular}}
+  %\rput(6.1,0.5){\begin{tabular}{l}non-empty\\[-1.6mm]subset\end{tabular}}
+  %\rput[c](1.7,1.5){$\lama$}
+  %\rput(3.7,1.75){isomorphism}
+  %\end{pspicture}
+  %\end{center}
+
+
 *}
 
 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
+  \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. 
@@ -44,7 +69,7 @@
   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>"}
+  @{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 
@@ -62,20 +87,28 @@
   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]}
+  @{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]}
+  @{thm[display,indent=5] fresh_def[no_vars]}
 
   \noindent
+  We also use for sets of atoms the abbreviation @{thm 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. For the proof we use the following lemma 
-  about swappings applied to an @{text x}:
+  @{text x} unchanged. 
+
+  \begin{Property}
+  @{thm[mode=IfThen] swap_fresh_fresh[no_vars]}
+  \end{Property}
+
+  \begin{Property}
+  @{thm[mode=IfThen] at_set_avoiding[no_vars]}
+  \end{Property}
 
 *}
 
@@ -91,9 +124,10 @@
 text {*
 
   \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.
+  {\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.
 
 
 *}