--- a/Paper/Paper.thy	Mon Mar 29 12:06:22 2010 +0200
+++ b/Paper/Paper.thy	Mon Mar 29 14:58:00 2010 +0200
@@ -229,7 +229,7 @@
   \emph{non}-alpha-equated, or ``raw'', terms. While our alpha-equated terms
   and the raw terms produced by Ott use names for bound variables,
   there is a key difference: working with alpha-equated terms means, for example,  
-  that the two type-schemes (with $x$, $y$ and $z$ being distinct)
+  that the two type-schemes
 
   \begin{center}
   @{text "\<forall>{x}. x \<rightarrow> y  = \<forall>{x, z}. x \<rightarrow> y"} 
@@ -329,7 +329,7 @@
   (Note that this means also the term-constructors for variables, applications
   and lambda are lifted to the quotient level.)  This construction, of course,
   only works if alpha-equivalence is indeed an equivalence relation, and the lifted
-  definitions and theorems are respectful w.r.t.~alpha-equivalence.  For exmple, we
+  definitions and theorems are respectful w.r.t.~alpha-equivalence.  For example, we
   will not be able to lift a bound-variable function, which can be defined for
   raw terms. The reason is that this function does not respect alpha-equivalence. 
   To sum up, every lifting of
@@ -363,7 +363,7 @@
   \begin{figure}
   \begin{boxedminipage}{\linewidth}
   \begin{center}
-  \begin{tabular}{rcl}
+  \begin{tabular}{r@ {\hspace{2mm}}cl}
   \multicolumn{3}{@ {}l}{Type Kinds}\\
   @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\medskip\\
   \multicolumn{3}{@ {}l}{Coercion Kinds}\\
@@ -383,7 +383,7 @@
   & & @{text "\<lambda>x:\<sigma>.e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 |"}\\
   & & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\medskip\\
   \multicolumn{3}{@ {}l}{Patterns}\\
-  @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
+  @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "a:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\medskip\\
   \multicolumn{3}{@ {}l}{Constants}\\
   @{text C} & & coercion constant\\
   @{text T} & & value type constructor\\
@@ -396,7 +396,7 @@
   \end{center}
   \end{boxedminipage}
   \caption{The term-language of System @{text "F\<^isub>C"}, also often referred to as Core-Haskell, 
-  according to \cite{CoreHaskell}. We only made an issential modification by 
+  according to \cite{CoreHaskell}. We only made an inessential modification by 
   separating the grammars for type kinds and coercion types.\label{corehas}}
   \end{figure}
 *}
@@ -495,9 +495,23 @@
   it can sometimes be difficult to establish the support precisely,
   and only give an over approximation (see functions above). This
   over approximation can be formalised with the notions \emph{supports},
-  defined as follows:
-  
+  defined as follows.
+
+  \begin{defn}
+  A set @{text S} \emph{supports} @{text x} if for all atoms @{text a} and @{text b}
+  not in @{text S} we have @{term "(a \<rightleftharpoons> b) \<bullet> x = x"}.
+  \end{defn}
 
+  \noindent
+  The point of this definitions is that we can show:
+
+  \begin{property}
+  {\it i)} @{thm[mode=IfThen] supp_is_subset[no_vars]} 
+  {\it ii)} @{thm supp_supports[no_vars]}.
+  \end{property}
+
+  \noindent
+  Another important notion in the nominal logic work is \emph{equivariance}.
 
   %\begin{property}
   %@{thm[mode=IfThen] at_set_avoiding[no_vars]}
@@ -749,7 +763,7 @@
 
   \noindent
   The point of these general lemmas about pairs is that we can define and prove properties 
-  about them conveninently on the Isabelle level, and in addition can use them in what
+  about them conveniently on the Isabelle level, and in addition can use them in what
   follows next when we have to deal with specific instances of term-specification. 
 *}
 
@@ -763,7 +777,7 @@
   @{text ty}$^\alpha_n$, and an associated collection
   of binding functions, say @{text bn}$^\alpha_1$, \ldots, @{text
   bn}$^\alpha_m$. The syntax in Nominal Isabelle for such specifications is
-  rougly as follows:
+  roughly as follows:
   %
   \begin{equation}\label{scheme}
   \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
@@ -930,7 +944,7 @@
   to determine whether the binder came from the binding function @{text
   "bn(p)"} or @{text "bn(q)"}. Similarly in the second case. There the binder
   @{text "bn(p)"} overlaps with the shallow binder @{text x}. The reason why
-  we must exclude such specifiactions is that they cannot be represent by
+  we must exclude such specifications is that they cannot be represent by
   the general binders described in Section \ref{sec:binders}. However
   the following two term-constructors are allowed
 
@@ -947,7 +961,7 @@
   since there is no overlap of binders.
   
   Note that in the last example we wrote {\it\isacommand{bind}\;bn(p)\;\isacommand{in}\;p}.
-  Whenver such a binding clause is present, we will call the binder \emph{recursive}.
+  Whenever such a binding clause is present, we will call the binder \emph{recursive}.
   To see the purpose for this, consider ``plain'' Lets and Let\_recs:
 
   \begin{center}
@@ -983,7 +997,7 @@
   then use the type constructors @{text "abs_set"}, @{text "abs_res"} and
   @{text "abs_list"} from Section \ref{sec:binders}. Therefore we will first
   extract datatype definitions from the specification and then define an
-  alpha-equiavlence relation over them.
+  alpha-equivalence relation over them.
 
 
   The datatype definition can be obtained by just stripping off the 
@@ -998,7 +1012,7 @@
   \noindent
   The resulting datatype definition is legal in Isabelle/HOL provided the datatypes are 
   non-empty and the types in the constructors only occur in positive 
-  position (see \cite{} for an indepth explanataion of the datatype package
+  position (see \cite{} for an indepth explanation of the datatype package
   in Isabelle/HOL). We then define the user-specified binding 
   functions by primitive recursion over the raw datatypes. We can also
   easily define a permutation operation by primitive recursion so that for each
@@ -1013,7 +1027,7 @@
   all permutation types (Def ??) by a simple structural induction over
   the @{text "ty_raw"}s.
 
-  The first non-trivial step we have to perform is the generatation free-variable 
+  The first non-trivial step we have to perform is the generation free-variable 
   functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
   we need to define the free-variable functions
 
@@ -1044,7 +1058,7 @@
   \begin{center}
   \begin{tabular}{cp{7cm}}
   $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
-  $\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder\\
+  $\bullet$ & @{text "ft_bn_by\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder\\
   $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep recursive binder\\
   \end{tabular}
   \end{center}