--- a/Nominal/Ex1rec.thy	Tue Mar 30 09:15:40 2010 +0200
+++ b/Nominal/Ex1rec.thy	Tue Mar 30 10:36:05 2010 +0200
@@ -5,6 +5,7 @@
 atom_decl name
 
 ML {* val _ = recursive := true *}
+ML {* val _ = alpha_type := AlphaGen *}
 nominal_datatype lam' =
   VAR' "name"
 | APP' "lam'" "lam'"

--- a/Paper/Paper.thy	Tue Mar 30 09:15:40 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 10:36:05 2010 +0200
@@ -1142,7 +1142,6 @@
 
 \marginpar{\small We really have @{text "bn_raw"}, @{text "fv_bn_raw"}. Should we mention this?}
 
-
   \noindent Next, for each binding function @{text "bn"} we define a
   free variable function @{text "fv_bn"}. The basic idea behind this
   function is to compute all the free atoms under this binding
@@ -1154,6 +1153,8 @@
   we define @{text "fv_bn"} to be the union of the values calculated
   for @{text "x\<^isub>j"} as follows:
 
+ \marginpar{raw for being defined}
+
   \begin{center}
   \begin{tabular}{cp{7cm}}
   $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\
@@ -1162,9 +1163,9 @@
   $\bullet$ & @{text "(atoms x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a set of atoms\\
   $\bullet$ & @{text "(atoml x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a list of atoms\\
   $\bullet$ & @{text "(fv_ty x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a nominal datatype
-    with a free variable function @{text "fv_ty"}. This includes the currently defined
-    types, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\
-  $\bullet$ & @{term "{}"} otherwise 
+    with a free variable function @{text "fv_ty"}. This includes the types being
+    defined, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\
+  $\bullet$ & @{term "{}"} otherwise
   \end{tabular}
   \end{center}
 
@@ -1182,7 +1183,31 @@
   @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"}
   \end{center}
 
+  TODO existance of permutations.
 
+  Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
+  of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if
+  the conjunction of equivalences for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
+  For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:
+
+  \begin{center}
+  \begin{tabular}{cp{7cm}}
+  $\bullet$ & @{text "x\<^isub>j"} is a shallow binder\\
+  $\bullet$ & @{text "x\<^isub>j \<approx>bn\<^isub>m y\<^isub>j"} provided @{text "x\<^isub>j"} is a deep non-recursive binder
+     with the auxiliary binding function @{text "bn\<^isub>m"}\\
+  $\bullet$ & @{text "(bn\<^isub>m x\<^isub>j, (x\<^isub>j, x)) \<approx>gen \<approx>s fvs pi (bn\<^isub>m y\<^isub>j, (y\<^isub>j, s)"}
+     provided @{text "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
+     function @{text "bn\<^isub>m"}, ...\\
+  $\bullet$ & @{text "(x\<^isub>n, x\<^isub>j) \<approx>gen \<approx> fv_ty pi (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>n"}
+     is bound in @{text "x\<^isub>j"} \\
+  $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
+  $\bullet$ & @{text "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen \<approx> fv_ty pi (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided  @{text "bn\<^isub>m x\<^isub>n"}
+    is bound non-recursively in @{text "x\<^isub>j"} \\
+  $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes
+    the types being defined, raw)\\
+  $\bullet$ & @{text "x\<^isub>j = y\<^isub>j"} otherwise\\
+  \end{tabular}
+  \end{center}
 
 
 *}