diff -r 5d145fe77ec1 -r 8146b0ad8212 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Aug 17 09:43:37 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Aug 17 21:08:48 2011 +0200
@@ -124,7 +124,7 @@
   that can be used to faithfully represent this kind of binding in Nominal
   Isabelle.  The difficulty of finding the right notion for alpha-equivalence
   can be appreciated in this case by considering that the definition given by
-  Leroy in \cite[Page ???]{Leroy92} is incorrect (it omits a side-condition).
+  Leroy in \cite[Page 18--19]{Leroy92} is incorrect (it omits a side-condition).
 
   However, the notion of alpha-equivalence that is preserved by vacuous
   binders is not always wanted. For example in terms like
@@ -319,6 +319,7 @@
   system. This package allows us to lift definitions and theorems involving
   raw terms to definitions and theorems involving alpha-equated terms. For
   example if we define the free-variable function over raw lambda-terms
+  as follows
 
   \[
   \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l}
@@ -356,12 +357,12 @@
   infrastructure for alpha-equated terms.\smallskip
 
   The examples we have in mind where our reasoning infrastructure will be
-  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. 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
+  helpful includes the term language of Core-Haskell (see
+  Figure~\ref{corehas}). This term language involves patterns that have lists
+  of type-, coercion- and term-variables, 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
@@ -380,47 +381,45 @@
   for our specifications from ``first principles''.
 
 
-  %\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}{@ {\hspace{8mm}}r@ {\hspace{2mm}}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> | refl \<sigma> | sym \<gamma> | \<gamma>\<^isub>1 \<circ> \<gamma>\<^isub>2"}\\
+  & @{text "|"} & @{text "\<gamma> @ \<sigma> | left \<gamma> | right \<gamma> | \<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> | \<lambda>x:\<sigma>. e | e\<^isub>1 e\<^isub>2"}\\
+  & @{text "|"} & @{text "\<LET> x:\<sigma> = e\<^isub>1 \<IN> e\<^isub>2 | \<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 *}
@@ -490,7 +489,7 @@
   Concrete permutations in Nominal Isabelle are built up from swappings, 
   written as \mbox{@{text "(a b)"}}, which are permutations that behave 
   as follows:
-  %
+  
   \begin{center}
   @{text "(a b) = \<lambda>c. if a = c then b else if b = c then a else c"}
   \end{center}
@@ -502,7 +501,7 @@
   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:
-  %
+  
   \begin{equation}\label{suppdef}
   @{thm supp_def[no_vars, THEN eq_reflection]}
   \end{equation}