
diff -r f5621efe5a20 -r 6d9018d62b40 Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Oct 04 07:25:37 2010 +0100
+++ b/Paper/Paper.thy	Mon Oct 04 12:39:57 2010 +0100
@@ -61,11 +61,11 @@
 
   So far, Nominal Isabelle provided a mechanism for constructing
   $\alpha$-equated terms, for example lambda-terms
-
+  %
   \begin{center}
   @{text "t ::= x | t t | \<lambda>x. t"}
   \end{center}
-
+  %
   \noindent
   where free and bound variables have names.  For such $\alpha$-equated terms,
   Nominal Isabelle derives automatically a reasoning infrastructure that has
@@ -87,7 +87,7 @@
   @{text "S ::= \<forall>{x\<^isub>1,\<dots>, x\<^isub>n}. T"}
   \end{array}
   \end{equation}
-
+  %
   \noindent
   and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
   type-variables.  While it is possible to implement this kind of more general
@@ -96,7 +96,7 @@
   why Nominal Isabelle and similar theorem provers that only provide
   mechanisms for binding single variables have not fared extremely well with the
   more advanced tasks in the POPLmark challenge \cite{challenge05}, because
-  also there one would like to bind multiple variables at once.
+  also there one would like to bind multiple variables at once. 
 
   Binding multiple variables has interesting properties that cannot be captured
   easily by iterating single binders. For example in the case of type-schemes we do not
@@ -106,7 +106,7 @@
   \begin{equation}\label{ex1}
   @{text "\<forall>{x, y}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{y, x}. x \<rightarrow> y"} 
   \end{equation}
-
+  %
   \noindent
   but assuming that @{text x}, @{text y} and @{text z} are distinct variables,
   the following two should \emph{not} be $\alpha$-equivalent
@@ -114,7 +114,7 @@
   \begin{equation}\label{ex2}
   @{text "\<forall>{x, y}. x \<rightarrow> y  \<notapprox>\<^isub>\<alpha>  \<forall>{z}. z \<rightarrow> z"} 
   \end{equation}
-
+  %
   \noindent
   Moreover, we like to regard type-schemes as $\alpha$-equivalent, if they differ
   only on \emph{vacuous} binders, such as
@@ -122,7 +122,7 @@
   \begin{equation}\label{ex3}
   @{text "\<forall>{x}. x \<rightarrow> y  \<approx>\<^isub>\<alpha>  \<forall>{x, z}. x \<rightarrow> y"}
   \end{equation}
-
+  %
   \noindent
   where @{text z} does not occur freely in the type.  In this paper we will
   give a general binding mechanism and associated notion of $\alpha$-equivalence
@@ -146,7 +146,7 @@
   \begin{center}
   @{text "\<LET> x = 3 \<AND> y = 2 \<AND> z = loop \<IN> x - y \<END>"}
   \end{center}
-
+  %
   \noindent
   Therefore we will also provide a separate binding mechanism for cases in
   which the order of binders does not matter, but the ``cardinality'' of the
@@ -159,7 +159,7 @@
   \begin{equation}\label{two}
   @{text "\<LET> (x, y) = (3, 2) \<IN> x - y \<END>"}
   \end{equation}
-
+  %
   \noindent
   we want to bind all variables from the pattern inside the body of the
   $\mathtt{let}$, but we also care about the order of these variables, since
@@ -172,7 +172,8 @@
   \noindent
   As a result, we provide three general binding mechanisms each of which binds
   multiple variables at once, and let the user chose which one is intended
-  when formalising a term-calculus.
+  in a formalisation.
+  %%when formalising a term-calculus.
 
   By providing these general binding mechanisms, however, we have to work
   around a problem that has been pointed out by Pottier \cite{Pottier06} and
@@ -181,18 +182,17 @@
   \begin{center}
   @{text "\<LET> x\<^isub>1 = t\<^isub>1 \<AND> \<dots> \<AND> x\<^isub>n = t\<^isub>n \<IN> s \<END>"}
   \end{center}
-
+  %
   \noindent
-  which bind all the @{text "x\<^isub>i"} in @{text s}, we might not care
-  about the order in which the @{text "x\<^isub>i = t\<^isub>i"} are given,
-  but we do care about the information that there are as many @{text
+  we care about the 
+  information that there are as many bound variables @{text
   "x\<^isub>i"} as there are @{text "t\<^isub>i"}. We lose this information if
   we represent the @{text "\<LET>"}-constructor by something like
   %
   \begin{center}
   @{text "\<LET> (\<lambda>x\<^isub>1\<dots>x\<^isub>n . s)  [t\<^isub>1,\<dots>,t\<^isub>n]"}
   \end{center}
-
+  %
   \noindent
   where the notation @{text "\<lambda>_ . _"} indicates that the list of @{text
   "x\<^isub>i"} becomes bound in @{text s}. In this representation the term
@@ -204,45 +204,47 @@
   allow type specifications for @{text "\<LET>"}s as follows
   %
   \begin{center}
-  \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}l}
-  @{text trm} & @{text "::="}  & @{text "\<dots>"}\\ 
-              & @{text "|"}    & @{text "\<LET>  as::assn  s::trm"}\hspace{4mm} 
+  \begin{tabular}{r@ {\hspace{2mm}}r@ {\hspace{2mm}}cl}
+  @{text trm} & @{text "::="}  & @{text "\<dots>"} 
+              & @{text "|"}  @{text "\<LET>  as::assn  s::trm"}\hspace{2mm} 
                                  \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}\\[1mm]
-  @{text assn} & @{text "::="} & @{text "\<ANIL>"}\\
-               & @{text "|"}   & @{text "\<ACONS>  name  trm  assn"}
+  @{text assn} & @{text "::="} & @{text "\<ANIL>"}
+               &  @{text "|"}  @{text "\<ACONS>  name  trm  assn"}
   \end{tabular}
   \end{center}
-
+  %
   \noindent
   where @{text assn} is an auxiliary type representing a list of assignments
   and @{text bn} an auxiliary function identifying the variables to be bound
   by the @{text "\<LET>"}. This function can be defined by recursion over @{text
   assn} as follows
-
+  %
   \begin{center}
   @{text "bn(\<ANIL>) ="} @{term "{}"} \hspace{5mm} 
   @{text "bn(\<ACONS> x t as) = {x} \<union> bn(as)"} 
   \end{center}
-  
+  %
   \noindent
   The scope of the binding is indicated by labels given to the types, for
   example @{text "s::trm"}, and a binding clause, in this case
   \isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "s"}. This binding
   clause states that all the names the function @{text
   "bn(as)"} returns should be bound in @{text s}.  This style of specifying terms and bindings is heavily
-  inspired by the syntax of the Ott-tool \cite{ott-jfp}. Though, Ott
-  has only one binding mode, namely the one where the order of
-  binders matters. Consequently, type-schemes with binding sets
-  of names cannot be modelled in Ott.
+  inspired by the syntax of the Ott-tool \cite{ott-jfp}. 
+
+  %Though, Ott
+  %has only one binding mode, namely the one where the order of
+  %binders matters. Consequently, type-schemes with binding sets
+  %of names cannot be modelled in Ott.
 
   However, we will not be able to cope with all specifications that are
   allowed by Ott. One reason is that Ott lets the user specify ``empty'' 
   types like
-
+  %
   \begin{center}
   @{text "t ::= t t | \<lambda>x. t"}
   \end{center}
-
+  %
   \noindent
   where no clause for variables is given. Arguably, such specifications make
   some sense in the context of Coq's type theory (which Ott supports), but not
@@ -279,12 +281,12 @@
 
   Although in informal settings a reasoning infrastructure for $\alpha$-equated
   terms is nearly always taken for granted, establishing it automatically in
-  the Isabelle/HOL theorem prover is a rather non-trivial task. For every
+  the Isabelle/HOL is a rather non-trivial task. For every
   specification we will need to construct a type containing as elements the
   $\alpha$-equated terms. To do so, we use the standard HOL-technique of defining
   a new type by identifying a non-empty subset of an existing type.  The
   construction we perform in Isabelle/HOL can be illustrated by the following picture:
-
+  %
   \begin{center}
   \begin{tikzpicture}
   %\draw[step=2mm] (-4,-1) grid (4,1);
@@ -308,7 +310,7 @@
 
   \end{tikzpicture}
   \end{center}
-
+  %
   \noindent
   We take as the starting point a definition of raw terms (defined as a
   datatype in Isabelle/HOL); then identify the $\alpha$-equivalence classes in
@@ -318,12 +320,12 @@
   in Isabelle/HOL and the property that our relation for $\alpha$-equivalence is
   indeed an equivalence relation).
 
-  The fact that we obtain an isomorphism between the new type and the
-  non-empty subset shows that the new type is a faithful representation of
-  $\alpha$-equated terms. That is not the case for example for terms using the
-  locally nameless representation of binders \cite{McKinnaPollack99}: in this
-  representation there are ``junk'' terms that need to be excluded by
-  reasoning about a well-formedness predicate.
+  %The fact that we obtain an isomorphism between the new type and the
+  %non-empty subset shows that the new type is a faithful representation of
+  %$\alpha$-equated terms. That is not the case for example for terms using the
+  %locally nameless representation of binders \cite{McKinnaPollack99}: in this
+  %representation there are ``junk'' terms that need to be excluded by
+  %reasoning about a well-formedness predicate.
 
   The problem with introducing a new type in Isabelle/HOL is that in order to
   be useful, a reasoning infrastructure needs to be ``lifted'' from the
@@ -335,8 +337,8 @@
   define the free-variable function over raw lambda-terms
 
   \begin{center}
-  @{text "fv(x) = {x}"}\hspace{10mm}
-  @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\[1mm]
+  @{text "fv(x) = {x}"}\hspace{8mm}
+  @{text "fv(t\<^isub>1 t\<^isub>2) = fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\hspace{8mm}
   @{text "fv(\<lambda>x.t) = fv(t) - {x}"}
   \end{center}
   
@@ -346,8 +348,8 @@
   lifted function is characterised by the equations
 
   \begin{center}
-  @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{10mm}
-  @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\[1mm]
+  @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{8mm}
+  @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\hspace{8mm}
   @{text "fv\<^sup>\<alpha>(\<lambda>x.t) = fv\<^sup>\<alpha>(t) - {x}"}
   \end{center}
 
@@ -365,14 +367,12 @@
   infrastructure for $\alpha$-equated terms.
 
   The examples we have in mind where our reasoning infrastructure will be
-  helpful includes the term language of System @{text "F\<^isub>C"}, also
-  known as Core-Haskell (see Figure~\ref{corehas}). This term language
+  helpful includes the term language of Core-Haskell. This term language
   involves patterns that have lists of type-, coercion- and term-variables,
-  all of which are bound in @{text "\<CASE>"}-expressions. One
-  feature is that we do not know in advance how many variables need to
-  be bound. Another is that each bound variable comes with a kind or type
-  annotation. Representing such binders with single binders and reasoning
-  about them in a theorem prover would be a major pain.  \medskip
+  all of which are bound in @{text "\<CASE>"}-expressions. In these
+  patterns we do not know in advance how many variables need to
+  be bound. Another example is the specification of SML, which includes
+  includes bindings as in type-schemes.\medskip
 
   \noindent
   {\bf Contributions:}  We provide three new definitions for when terms
@@ -384,53 +384,54 @@
   induction principles that have the variable convention already built in.
   The method behind our specification of general binders is taken 
   from the Ott-tool, but we introduce crucial restrictions, and also extensions, so 
-  that our specifications make sense for reasoning about $\alpha$-equated terms.  The main improvement over Ott is that we introduce three binding modes,
-   provide precise definitions for $\alpha$-equivalence and for free
-   variables of our terms, and provide automated proofs inside the
-   Isabelle theorem prover.
+  that our specifications make sense for reasoning about $\alpha$-equated terms.  
+  The main improvement over Ott is that we introduce three binding modes
+  (only one is present in Ott), provide definitions for $\alpha$-equivalence and 
+  for free variables of our terms, and also derive a reasoning infrastructure
+  about our specifications inside Isabelle/HOL.
 
 
-  \begin{figure}
-  \begin{boxedminipage}{\linewidth}
-  \begin{center}
-  \begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}
-  \multicolumn{3}{@ {}l}{Type Kinds}\\
-  @{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
-  \multicolumn{3}{@ {}l}{Coercion Kinds}\\
-  @{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
-  \multicolumn{3}{@ {}l}{Types}\\
-  @{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"} 
-  @{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
-  \multicolumn{3}{@ {}l}{Coercion Types}\\
-  @{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
-  @{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\
-  & @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
-  & @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
-  \multicolumn{3}{@ {}l}{Terms}\\
-  @{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\
-  & @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
-  & @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\
-  \multicolumn{3}{@ {}l}{Patterns}\\
-  @{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\
-  \multicolumn{3}{@ {}l}{Constants}\\
-  & @{text C} & coercion constants\\
-  & @{text T} & value type constructors\\
-  & @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\
-  & @{text K} & data constructors\smallskip\\
-  \multicolumn{3}{@ {}l}{Variables}\\
-  & @{text a} & type variables\\
-  & @{text c} & coercion variables\\
-  & @{text x} & term variables\\
-  \end{tabular}
-  \end{center}
-  \end{boxedminipage}
-  \caption{The System @{text "F\<^isub>C"}
-  \cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
-  version of @{text "F\<^isub>C"} we made a modification by separating the
-  grammars for type kinds and coercion kinds, as well as for types and coercion
-  types. For this paper the interesting term-constructor is @{text "\<CASE>"},
-  which binds multiple type-, coercion- and term-variables.\label{corehas}}
-  \end{figure}
+  %\begin{figure}
+  %\begin{boxedminipage}{\linewidth}
+  %%\begin{center}
+  %\begin{tabular}{r@ {\hspace{1mm}}r@ {\hspace{2mm}}l}
+  %\multicolumn{3}{@ {}l}{Type Kinds}\\
+  %@{text "\<kappa>"} & @{text "::="} & @{text "\<star> | \<kappa>\<^isub>1 \<rightarrow> \<kappa>\<^isub>2"}\smallskip\\
+  %\multicolumn{3}{@ {}l}{Coercion Kinds}\\
+  %@{text "\<iota>"} & @{text "::="} & @{text "\<sigma>\<^isub>1 \<sim> \<sigma>\<^isub>2"}\smallskip\\
+  %\multicolumn{3}{@ {}l}{Types}\\
+  %@{text "\<sigma>"} & @{text "::="} & @{text "a | T | \<sigma>\<^isub>1 \<sigma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<sigma>"}}$@{text "\<^sup>n"} 
+  %@{text "| \<forall>a:\<kappa>. \<sigma> | \<iota> \<Rightarrow> \<sigma>"}\smallskip\\
+  %\multicolumn{3}{@ {}l}{Coercion Types}\\
+  %@{text "\<gamma>"} & @{text "::="} & @{text "c | C | \<gamma>\<^isub>1 \<gamma>\<^isub>2 | S\<^isub>n"}$\;\overline{@{text "\<gamma>"}}$@{text "\<^sup>n"}
+  %@{text "| \<forall>c:\<iota>. \<gamma> | \<iota> \<Rightarrow> \<gamma> "}\\
+  %& @{text "|"} & @{text "refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2 | \<gamma> @ \<sigma> | left \<gamma> | right \<gamma>"}\\
+  %& @{text "|"} & @{text "\<gamma>\<^isub>1 \<sim> \<gamma>\<^isub>2 | rightc \<gamma> | leftc \<gamma> | \<gamma>\<^isub>1 \<triangleright> \<gamma>\<^isub>2"}\smallskip\\
+  %\multicolumn{3}{@ {}l}{Terms}\\
+  %@{text "e"} & @{text "::="} & @{text "x | K | \<Lambda>a:\<kappa>. e | \<Lambda>c:\<iota>. e | e \<sigma> | e \<gamma>"}\\
+  %& @{text "|"} & @{text "\<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2 | \<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2"}\\
+  %& @{text "|"} & @{text "\<CASE> e\<^isub>1 \<OF>"}$\;\overline{@{text "p \<rightarrow> e\<^isub>2"}}$ @{text "| e \<triangleright> \<gamma>"}\smallskip\\
+  %\multicolumn{3}{@ {}l}{Patterns}\\
+  %@{text "p"} & @{text "::="} & @{text "K"}$\;\overline{@{text "a:\<kappa>"}}\;\overline{@{text "c:\<iota>"}}\;\overline{@{text "x:\<sigma>"}}$\smallskip\\
+  %\multicolumn{3}{@ {}l}{Constants}\\
+  %& @{text C} & coercion constants\\
+  %& @{text T} & value type constructors\\
+  %& @{text "S\<^isub>n"} & n-ary type functions (which need to be fully applied)\\
+  %& @{text K} & data constructors\smallskip\\
+  %\multicolumn{3}{@ {}l}{Variables}\\
+  %& @{text a} & type variables\\
+  %& @{text c} & coercion variables\\
+  %& @{text x} & term variables\\
+  %\end{tabular}
+  %\end{center}
+  %\end{boxedminipage}
+  %\caption{The System @{text "F\<^isub>C"}
+  %\cite{CoreHaskell}, also often referred to as \emph{Core-Haskell}. In this
+  %version of @{text "F\<^isub>C"} we made a modification by separating the
+  %grammars for type kinds and coercion kinds, as well as for types and coercion
+  %types. For this paper the interesting term-constructor is @{text "\<CASE>"},
+  %which binds multiple type-, coercion- and term-variables.\label{corehas}}
+  %\end{figure}
 *}
 
 section {* A Short Review of the Nominal Logic Work *}
@@ -454,12 +455,7 @@
   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
-  %
-  \begin{center}
   @{text "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-  \end{center}
-
-  \noindent 
   in which the generic type @{text "\<beta>"} stands for the type of the object 
   over which the permutation 
   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
@@ -470,7 +466,7 @@
   given by:
   %
   \begin{equation}\label{permute}
-  \mbox{\begin{tabular}{@ {}cc@ {}}
+  \mbox{\begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
   \begin{tabular}{@ {}l@ {}}
   @{thm permute_prod.simps[no_vars, THEN eq_reflection]}\\[2mm]
   @{thm permute_list.simps(1)[no_vars, THEN eq_reflection]}\\
@@ -479,7 +475,7 @@
   \begin{tabular}{@ {}l@ {}}
   @{thm permute_set_eq[no_vars, THEN eq_reflection]}\\
   @{text "p \<bullet> f \<equiv> \<lambda>x. p \<bullet> (f (- p \<bullet> x))"}\\
-  @{thm permute_bool_def[no_vars, THEN eq_reflection]}\\
+  @{thm permute_bool_def[no_vars, THEN eq_reflection]}
   \end{tabular}
   \end{tabular}}
   \end{equation}
@@ -507,13 +503,7 @@
 
   \noindent
   There is also the derived notion for when an atom @{text a} is \emph{fresh}
-  for an @{text x}, defined as
-  %
-  \begin{center}
-  @{thm fresh_def[no_vars]}
-  \end{center}
-
-  \noindent
+  for an @{text x}, defined as @{thm fresh_def[no_vars]}.
   We use for sets of atoms the abbreviation 
   @{thm (lhs) fresh_star_def[no_vars]}, defined as 
   @{thm (rhs) fresh_star_def[no_vars]}.
@@ -530,65 +520,74 @@
   described, for example for atoms, products, lists, function applications, 
   booleans and permutations as follows
   %
-  \begin{eqnarray}
-  @{term "supp a"} & = & @{term "{a}"}\\
-  @{term "supp (x, y)"} & = & @{term "supp x \<union> supp y"}\\
-  @{term "supp []"} & = & @{term "{}"}\\
-  @{term "supp (x#xs)"} & = & @{term "supp x \<union> supp xs"}\\
-  @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\label{suppfun}\\
-  @{term "supp b"} & = & @{term "{}"}\\
-  @{term "supp p"} & = & @{term "{a. p \<bullet> a \<noteq> a}"}
-  \end{eqnarray}
+  \begin{center}
+  \begin{tabular}{c@ {\hspace{10mm}}c}
+  \begin{tabular}{rcl}
+  @{term "supp a"} & $=$ & @{term "{a}"}\\
+  @{term "supp (x, y)"} & $=$ & @{term "supp x \<union> supp y"}\\
+  @{term "supp []"} & $=$ & @{term "{}"}\\
+  @{term "supp (x#xs)"} & $=$ & @{term "supp x \<union> supp xs"}\\
+  \end{tabular}
+  &
+  \begin{tabular}{rcl}
+  @{text "supp (f x)"} & @{text "\<subseteq>"} & @{term "supp f \<union> supp x"}\\
+  @{term "supp b"} & $=$ & @{term "{}"}\\
+  @{term "supp p"} & $=$ & @{term "{a. p \<bullet> a \<noteq> a}"}
+  \end{tabular}
+  \end{tabular}
+  \end{center}
   
   \noindent 
   in some cases it can be difficult to characterise the support precisely, and
-  only an approximation can be established (see \eqref{suppfun} above). Reasoning about
-  such approximations can be simplified with the notion \emph{supports}, defined 
-  as follows:
-
-  \begin{definition}
-  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{definition}
+  only an approximation can be established (as for functions above). 
 
-  \noindent
-  The main point of @{text supports} is that we can establish the following 
-  two properties.
-
-  \begin{property}\label{supportsprop}
-  Given a set @{text "as"} of atoms.
-  {\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
-  {\it (ii)} @{thm supp_supports[no_vars]}.
-  \end{property}
-
-  Another important notion in the nominal logic work is \emph{equivariance}.
-  For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 
-  it is required that every permutation leaves @{text f} unchanged, that is
+  %Reasoning about
+  %such approximations can be simplified with the notion \emph{supports}, defined 
+  %as follows:
+  %
+  %\begin{definition}
+  %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{definition}
+  %
+  %\noindent
+  %The main point of @{text supports} is that we can establish the following 
+  %two properties.
+  %
+  %\begin{property}\label{supportsprop}
+  %Given a set @{text "as"} of atoms.
+  %{\it (i)} @{thm[mode=IfThen] supp_is_subset[where S="as", no_vars]}
+  %{\it (ii)} @{thm supp_supports[no_vars]}.
+  %\end{property}
   %
-  \begin{equation}\label{equivariancedef}
-  @{term "\<forall>p. p \<bullet> f = f"}
-  \end{equation}
-
-  \noindent or equivalently that a permutation applied to the application
-  @{text "f x"} can be moved to the argument @{text x}. That means for equivariant
-  functions @{text f}, we have for all permutations @{text p}:
+  %Another important notion in the nominal logic work is \emph{equivariance}.
+  %For a function @{text f}, say of type @{text "\<alpha> \<Rightarrow> \<beta>"}, to be equivariant 
+  %it is required that every permutation leaves @{text f} unchanged, that is
+  %%
+  %\begin{equation}\label{equivariancedef}
+  %@{term "\<forall>p. p \<bullet> f = f"}
+  %\end{equation}
   %
-  \begin{equation}\label{equivariance}
-  @{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
-  @{text "p \<bullet> (f x) = f (p \<bullet> x)"}
-  \end{equation}
- 
-  \noindent
-  From property \eqref{equivariancedef} and the definition of @{text supp}, we 
-  can easily deduce that equivariant functions have empty support. There is
-  also a similar notion for equivariant relations, say @{text R}, namely the property
-  that
-  %
-  \begin{center}
-  @{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
-  \end{center}
+  %\noindent or equivalently that a permutation applied to the application
+  %@{text "f x"} can be moved to the argument @{text x}. That means for equivariant
+  %functions @{text f}, we have for all permutations @{text p}:
+  %%
+  %\begin{equation}\label{equivariance}
+  %@{text "p \<bullet> f = f"} \;\;\;\textit{if and only if}\;\;\;
+  %@{text "p \<bullet> (f x) = f (p \<bullet> x)"}
+  %\end{equation}
+  % 
+  %\noindent
+  %From property \eqref{equivariancedef} and the definition of @{text supp}, we 
+  %can easily deduce that equivariant functions have empty support. There is
+  %also a similar notion for equivariant relations, say @{text R}, namely the property
+  %that
+  %%
+  %\begin{center}
+  %@{text "x R y"} \;\;\textit{implies}\;\; @{text "(p \<bullet> x) R (p \<bullet> y)"}
+  %\end{center}
 
-  Finally, the nominal logic work provides us with general means for renaming 
+  Using support and freshness, the nominal logic work provides us with general means for renaming 
   binders. While in the older version of Nominal Isabelle, we used extensively 
   Property~\ref{swapfreshfresh} to rename single binders, this property 
   proved too unwieldy for dealing with multiple binders. For such binders the 
@@ -649,15 +648,15 @@
   {\it (iii)} ``moves'' their bound names so that we obtain modulo a relation,
   say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it (iv)}
   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
-  requirements {\it (i)} to {\it (iv)} can be stated formally as follows:
+  requirements {\it (i)} to {\it (iv)} can be stated formally as the conjunction of:
   %
   \begin{equation}\label{alphaset}
-  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
-  \multicolumn{3}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-              & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
-  @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
-  @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
-  @{text "\<and>"} & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ 
+  \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
+  \multicolumn{4}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+       \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} &
+       \mbox{\it (iii)} &  @{text "(p \<bullet> x) R y"} \\
+       \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"} & 
+       \mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"} \\ 
   \end{array}
   \end{equation}
 
@@ -677,12 +676,12 @@
   as follows
   %
   \begin{equation}\label{alphalist}
-  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
-  \multicolumn{2}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-             & @{term "fa(x) - (set as) = fa(y) - (set bs)"} & \mbox{\it (i)}\\
-  \wedge     & @{term "(fa(x) - set as) \<sharp>* p"} & \mbox{\it (ii)}\\
-  \wedge     & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
-  \wedge     & @{term "(p \<bullet> as) = bs"} & \mbox{\it (iv)}\\ 
+  \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
+  \multicolumn{4}{l}{@{term "(as, x) \<approx>lst R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+         \mbox{\it (i)}   & @{term "fa(x) - (set as) = fa(y) - (set bs)"} & 
+         \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
+         \mbox{\it (ii)}  & @{term "(fa(x) - set as) \<sharp>* p"} &
+         \mbox{\it (iv)}  & @{term "(p \<bullet> as) = bs"}\\
   \end{array}
   \end{equation}
   
@@ -696,11 +695,11 @@
   condition in \eqref{alphaset}:
   %
   \begin{equation}\label{alphares}
-  \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
+  \begin{array}{@ {\hspace{10mm}}l@ {\hspace{5mm}}l@ {\hspace{10mm}}l@ {\hspace{5mm}}l}
   \multicolumn{2}{l}{@{term "(as, x) \<approx>res R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
-             & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
-  \wedge     & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
-  \wedge     & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
+             \mbox{\it (i)}   & @{term "fa(x) - as = fa(y) - bs"} & 
+             \mbox{\it (iii)} & @{text "(p \<bullet> x) R y"}\\
+             \mbox{\it (ii)}  & @{term "(fa(x) - as) \<sharp>* p"}\\
   \end{array}
   \end{equation}
 
@@ -780,90 +779,92 @@
   abstractions, namely:
 
   \begin{theorem}[Support of Abstractions]\label{suppabs} 
-  Assuming @{text x} has finite support, then\\[-6mm] 
+  Assuming @{text x} has finite support, then
+
   \begin{center}
-  \begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{thm (lhs) supp_Abs(1)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(1)[no_vars]}\\
-  @{thm (lhs) supp_Abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_Abs(2)[no_vars]}\\
-  @{thm (lhs) supp_Abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_Abs(3)[where bs="as", no_vars]}
+  \begin{tabular}{l}
+  @{thm (lhs) supp_Abs(1)[no_vars]} $=$
+  @{thm supp_Abs(2)[no_vars]}, and\\
+  @{thm supp_Abs(3)[where bs="as", no_vars]}
   \end{tabular}
   \end{center}
   \end{theorem}
 
   \noindent
-  Below we will show the first equation. The others 
-  follow by similar arguments. By definition of the abstraction type @{text "abs_set"} 
-  we have 
-  %
-  \begin{equation}\label{abseqiff}
-  @{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; 
-  @{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
-  \end{equation}
-
-  \noindent
-  and also
-  %
-  \begin{equation}\label{absperm}
-  @{thm permute_Abs[no_vars]}
-  \end{equation}
+  This theorem states that the bound names do not appear in the support, as expected.
+  For brevity we omit the proof of this resul and again refer the reader to
+  our formalisation in Isabelle/HOL.
 
-  \noindent
-  The second fact derives from the definition of permutations acting on pairs 
-  \eqref{permute} and $\alpha$-equivalence being equivariant 
-  (see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show 
-  the following lemma about swapping two atoms in an abstraction.
-  
-  \begin{lemma}
-  @{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
-  \end{lemma}
+  %\noindent
+  %Below we will show the first equation. The others 
+  %follow by similar arguments. By definition of the abstraction type @{text "abs_set"} 
+  %we have 
+  %%
+  %\begin{equation}\label{abseqiff}
+  %@{thm (lhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]} \;\;\text{if and only if}\;\; 
+  %@{thm (rhs) Abs_eq_iff(1)[where bs="as" and cs="bs", no_vars]}
+  %\end{equation}
+  %
+  %\noindent
+  %and also
+  %
+  %\begin{equation}\label{absperm}
+  %%@%{%thm %permute_Abs[no_vars]}%
+  %\end{equation}
 
-  \begin{proof}
-  This lemma is straightforward using \eqref{abseqiff} and observing that
-  the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
-  Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
-  \end{proof}
-
-  \noindent
-  Assuming that @{text "x"} has finite support, this lemma together 
-  with \eqref{absperm} allows us to show
+  %\noindent
+  %The second fact derives from the definition of permutations acting on pairs 
+  %\eqref{permute} and $\alpha$-equivalence being equivariant 
+  %(see Lemma~\ref{alphaeq}). With these two facts at our disposal, we can show 
+  %the following lemma about swapping two atoms in an abstraction.
+  %
+  %\begin{lemma}
+  %@{thm[mode=IfThen] Abs_swap1(1)[where bs="as", no_vars]}
+  %\end{lemma}
+  %
+  %\begin{proof}
+  %This lemma is straightforward using \eqref{abseqiff} and observing that
+  %the assumptions give us @{term "(a \<rightleftharpoons> b) \<bullet> (supp x - as) = (supp x - as)"}.
+  %Moreover @{text supp} and set difference are equivariant (see \cite{HuffmanUrban10}).
+  %\end{proof}
   %
-  \begin{equation}\label{halfone}
-  @{thm Abs_supports(1)[no_vars]}
-  \end{equation}
-  
-  \noindent
-  which by Property~\ref{supportsprop} gives us ``one half'' of
-  Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish 
-  it, we use a trick from \cite{Pitts04} and first define an auxiliary 
-  function @{text aux}, taking an abstraction as argument:
+  %\noindent
+  %Assuming that @{text "x"} has finite support, this lemma together 
+  %with \eqref{absperm} allows us to show
+  %
+  %\begin{equation}\label{halfone}
+  %@{thm Abs_supports(1)[no_vars]}
+  %\end{equation}
+  %
+  %\noindent
+  %which by Property~\ref{supportsprop} gives us ``one half'' of
+  %Theorem~\ref{suppabs}. The ``other half'' is a bit more involved. To establish 
+  %it, we use a trick from \cite{Pitts04} and first define an auxiliary 
+  %function @{text aux}, taking an abstraction as argument:
+  %@{thm supp_set.simps[THEN eq_reflection, no_vars]}.
   %
-  \begin{center}
-  @{thm supp_set.simps[THEN eq_reflection, no_vars]}
-  \end{center}
-  
-  \noindent
-  Using the second equation in \eqref{equivariance}, we can show that 
-  @{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) =
-  (supp (p \<bullet> x)) - (p \<bullet> as)"}) and therefore has empty support. 
-  This in turn means
+  %Using the second equation in \eqref{equivariance}, we can show that 
+  %@{text "aux"} is equivariant (since @{term "p \<bullet> (supp x - as) = (supp (p \<bullet> x)) - (p \<bullet> as)"}) 
+  %and therefore has empty support. 
+  %This in turn means
+  %
+  %\begin{center}
+  %@{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
+  %\end{center}
   %
-  \begin{center}
-  @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
-  \end{center}
-
-  \noindent
-  using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
-  we further obtain
+  %\noindent
+  %using \eqref{suppfun}. Assuming @{term "supp x - as"} is a finite set,
+  %we further obtain
   %
-  \begin{equation}\label{halftwo}
-  @{thm (concl) Abs_supp_subset1(1)[no_vars]}
-  \end{equation}
-
-  \noindent
-  since for finite sets of atoms, @{text "bs"}, we have 
-  @{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
-  Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
-  Theorem~\ref{suppabs}. 
+  %\begin{equation}\label{halftwo}
+  %@{thm (concl) Abs_supp_subset1(1)[no_vars]}
+  %\end{equation}
+  %
+  %\noindent
+  %since for finite sets of atoms, @{text "bs"}, we have 
+  %@{thm (concl) supp_finite_atom_set[where S="bs", no_vars]}.
+  %Finally, taking \eqref{halfone} and \eqref{halftwo} together establishes 
+  %Theorem~\ref{suppabs}. 
 
   The method of first considering abstractions of the
   form @{term "Abs_set as x"} etc is motivated by the fact that 
@@ -886,7 +887,7 @@
   syntax in Nominal Isabelle for such specifications is roughly as follows:
   %
   \begin{equation}\label{scheme}
-  \mbox{\begin{tabular}{@ {\hspace{-5mm}}p{1.8cm}l}
+  \mbox{\begin{tabular}{@ {}p{2.5cm}l}
   type \mbox{declaration part} &
   $\begin{cases}
   \mbox{\begin{tabular}{l}
@@ -987,8 +988,8 @@
 
 
   \begin{center}
-  \begin{tabular}{@ {}cc@ {}}
-  \begin{tabular}{@ {}l@ {\hspace{-2mm}}}
+  \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
+  \begin{tabular}{@ {}l}
   \isacommand{nominal\_datatype} @{text lam} $=$\\
   \hspace{5mm}\phantom{$\mid$}~@{text "Var name"}\\
   \hspace{5mm}$\mid$~@{text "App lam lam"}\\
@@ -1210,7 +1211,7 @@
   \end{equation}
 
   \noindent
-  by mutual recursion.
+  by recursion.
   We define these functions together with auxiliary free-atom functions for
   the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ 
   we define
@@ -1809,74 +1810,74 @@
   are generated automatically by custom ML-code. This code can deal with 
   specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.  
 
-  \begin{figure}[t!]
-  \begin{boxedminipage}{\linewidth}
-  \small
-  \begin{tabular}{l}
-  \isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
-  \isacommand{nominal\_datatype}~@{text "tkind ="}\\
-  \phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ 
-  \isacommand{and}~@{text "ckind ="}\\
-  \phantom{$|$}~@{text "CKSim ty ty"}\\
-  \isacommand{and}~@{text "ty ="}\\
-  \phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
-  $|$~@{text "TFun string ty_list"}~%
-  $|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
-  $|$~@{text "TArr ckind ty"}\\
-  \isacommand{and}~@{text "ty_lst ="}\\
-  \phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
-  \isacommand{and}~@{text "cty ="}\\
-  \phantom{$|$}~@{text "CVar cvar"}~%
-  $|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
-  $|$~@{text "CAll cv::cvar ckind cty::cty"}  \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\
-  $|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
-  $|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
-  $|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
-  \isacommand{and}~@{text "co_lst ="}\\
-  \phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
-  \isacommand{and}~@{text "trm ="}\\
-  \phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
-  $|$~@{text "LAM_ty tv::tvar tkind t::trm"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
-  $|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
-  $|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
-  $|$~@{text "Lam v::var ty t::trm"}  \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
-  $|$~@{text "Let x::var ty trm t::trm"}  \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
-  $|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
-  \isacommand{and}~@{text "assoc_lst ="}\\
-  \phantom{$|$}~@{text ANil}~%
-  $|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
-  \isacommand{and}~@{text "pat ="}\\
-  \phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
-  \isacommand{and}~@{text "vt_lst ="}\\
-  \phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
-  \isacommand{and}~@{text "tvtk_lst ="}\\
-  \phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
-  \isacommand{and}~@{text "tvck_lst ="}\\ 
-  \phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
-  \isacommand{binder}\\
-  @{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
-  @{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
-  @{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
-  @{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
-  \isacommand{where}\\
-  \phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
-  $|$~@{text "bv1 VTNil = []"}\\
-  $|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
-  $|$~@{text "bv2 TVTKNil = []"}\\
-  $|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
-  $|$~@{text "bv3 TVCKNil = []"}\\
-  $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
-  \end{tabular}
-  \end{boxedminipage}
-  \caption{The nominal datatype declaration for Core-Haskell. For the moment we
-  do not support nested types; therefore we explicitly have to unfold the 
-  lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved
-  in a future version of Nominal Isabelle. Apart from that, the 
-  declaration follows closely the original in Figure~\ref{corehas}. The
-  point of our work is that having made such a declaration in Nominal Isabelle,
-  one obtains automatically a reasoning infrastructure for Core-Haskell.
-  \label{nominalcorehas}}
-  \end{figure}
+  %\begin{figure}[t!]
+  %\begin{boxedminipage}{\linewidth}
+  %\small
+  %\begin{tabular}{l}
+  %\isacommand{atom\_decl}~@{text "var cvar tvar"}\\[1mm]
+  %\isacommand{nominal\_datatype}~@{text "tkind ="}\\
+  %\phantom{$|$}~@{text "KStar"}~$|$~@{text "KFun tkind tkind"}\\ 
+  %\isacommand{and}~@{text "ckind ="}\\
+  %\phantom{$|$}~@{text "CKSim ty ty"}\\
+  %\isacommand{and}~@{text "ty ="}\\
+  %\phantom{$|$}~@{text "TVar tvar"}~$|$~@{text "T string"}~$|$~@{text "TApp ty ty"}\\
+  %$|$~@{text "TFun string ty_list"}~%
+  %$|$~@{text "TAll tv::tvar tkind ty::ty"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text ty}\\
+  %$|$~@{text "TArr ckind ty"}\\
+  %\isacommand{and}~@{text "ty_lst ="}\\
+  %\phantom{$|$}~@{text "TNil"}~$|$~@{text "TCons ty ty_lst"}\\
+  %\isacommand{and}~@{text "cty ="}\\
+  %\phantom{$|$}~@{text "CVar cvar"}~%
+  %$|$~@{text "C string"}~$|$~@{text "CApp cty cty"}~$|$~@{text "CFun string co_lst"}\\
+  %$|$~@{text "CAll cv::cvar ckind cty::cty"}  \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text cty}\\
+  %$|$~@{text "CArr ckind cty"}~$|$~@{text "CRefl ty"}~$|$~@{text "CSym cty"}~$|$~@{text "CCirc cty cty"}\\
+  %$|$~@{text "CAt cty ty"}~$|$~@{text "CLeft cty"}~$|$~@{text "CRight cty"}~$|$~@{text "CSim cty cty"}\\
+  %$|$~@{text "CRightc cty"}~$|$~@{text "CLeftc cty"}~$|$~@{text "Coerce cty cty"}\\
+  %\isacommand{and}~@{text "co_lst ="}\\
+  %\phantom{$|$}@{text "CNil"}~$|$~@{text "CCons cty co_lst"}\\
+  %\isacommand{and}~@{text "trm ="}\\
+  %\phantom{$|$}~@{text "Var var"}~$|$~@{text "K string"}\\
+  %$|$~@{text "LAM_ty tv::tvar tkind t::trm"}  \isacommand{bind}~@{text "tv"}~\isacommand{in}~@{text t}\\
+  %$|$~@{text "LAM_cty cv::cvar ckind t::trm"}   \isacommand{bind}~@{text "cv"}~\isacommand{in}~@{text t}\\
+  %$|$~@{text "App_ty trm ty"}~$|$~@{text "App_cty trm cty"}~$|$~@{text "App trm trm"}\\
+  %$|$~@{text "Lam v::var ty t::trm"}  \isacommand{bind}~@{text "v"}~\isacommand{in}~@{text t}\\
+  %$|$~@{text "Let x::var ty trm t::trm"}  \isacommand{bind}~@{text x}~\isacommand{in}~@{text t}\\
+  %$|$~@{text "Case trm assoc_lst"}~$|$~@{text "Cast trm co"}\\
+  %\isacommand{and}~@{text "assoc_lst ="}\\
+  %\phantom{$|$}~@{text ANil}~%
+  %$|$~@{text "ACons p::pat t::trm assoc_lst"}  \isacommand{bind}~@{text "bv p"}~\isacommand{in}~@{text t}\\
+  %\isacommand{and}~@{text "pat ="}\\
+  %\phantom{$|$}~@{text "Kpat string tvtk_lst tvck_lst vt_lst"}\\
+  %\isacommand{and}~@{text "vt_lst ="}\\
+  %\phantom{$|$}~@{text VTNil}~$|$~@{text "VTCons var ty vt_lst"}\\
+  %\isacommand{and}~@{text "tvtk_lst ="}\\
+  %\phantom{$|$}~@{text TVTKNil}~$|$~@{text "TVTKCons tvar tkind tvtk_lst"}\\
+  %\isacommand{and}~@{text "tvck_lst ="}\\ 
+  %\phantom{$|$}~@{text TVCKNil}~$|$ @{text "TVCKCons cvar ckind tvck_lst"}\\
+  %\isacommand{binder}\\
+  %@{text "bv :: pat \<Rightarrow> atom list"}~\isacommand{and}~%
+  %@{text "bv1 :: vt_lst \<Rightarrow> atom list"}~\isacommand{and}\\
+  %@{text "bv2 :: tvtk_lst \<Rightarrow> atom list"}~\isacommand{and}~%
+  %@{text "bv3 :: tvck_lst \<Rightarrow> atom list"}\\
+  %\isacommand{where}\\
+  %\phantom{$|$}~@{text "bv (K s tvts tvcs vs) = (bv3 tvts) @ (bv2 tvcs) @ (bv1 vs)"}\\
+  %$|$~@{text "bv1 VTNil = []"}\\
+  %$|$~@{text "bv1 (VTCons x ty tl) = (atom x)::(bv1 tl)"}\\
+  %$|$~@{text "bv2 TVTKNil = []"}\\
+  %$|$~@{text "bv2 (TVTKCons a ty tl) = (atom a)::(bv2 tl)"}\\
+  %$|$~@{text "bv3 TVCKNil = []"}\\
+  %$|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
+  %\end{tabular}
+  %\end{boxedminipage}
+  %\caption{The nominal datatype declaration for Core-Haskell. For the moment we
+  %do not support nested types; therefore we explicitly have to unfold the 
+  %lists @{text "co_lst"}, @{text "assoc_lst"} and so on. This will be improved
+  %in a future version of Nominal Isabelle. Apart from that, the 
+  %declaration follows closely the original in Figure~\ref{corehas}. The
+  %point of our work is that having made such a declaration in Nominal Isabelle,
+  %one obtains automatically a reasoning infrastructure for Core-Haskell.
+  %\label{nominalcorehas}}
+  %\end{figure}
 *}
 
 




