--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/PAPER-TODO	Mon Apr 19 15:37:33 2010 +0200
@@ -0,0 +1,20 @@
+_{res} -> _{\textrm{res}} etc.; same for =^{def}?
+
+Nominal Isabelle view, rather than functional programming view
+(e.g. first sentence of Abstract and Intro)
+
+
+:: for cons might need some explanations, esp. that it's also used later
+next to labels in nominal types (e.g. x::name t::lam).
+
+
+Ott-tool -> Ott tool (throughout)
+
+I didn't quite get top of second column, p. 6
+
+"the problem Pottier and Cheney pointed out": I had forgotten it in the
+meantime
+
+the equation in the first actuall bullet on p. 8 lacks it =?
+
+missing v. spaces, top of 2nd col p. 8
\ No newline at end of file

--- a/Paper/Paper.thy	Mon Apr 19 12:28:48 2010 +0200
+++ b/Paper/Paper.thy	Mon Apr 19 15:37:33 2010 +0200
@@ -441,7 +441,7 @@
   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
   the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, 
   and the inverse permutation of @{term p} as @{text "- p"}. The permutation
-  operation is defined by induction over the type-hierarchy (see \cite{HuffmanUrban10});
+  operation is defined by induction over the type-hierarchy \cite{HuffmanUrban10};
   for example permutations acting on products, lists, sets, functions and booleans is
   given by:
   %
@@ -614,7 +614,7 @@
   "as"} in the body @{text "x"}.
 
   The first question we have to answer is when two pairs @{text "(as, x)"} and
-  @{text "(bs, y)"} are alpha-equivalent? (At the moment we are interested in
+  @{text "(bs, y)"} are alpha-equivalent? (For the moment we are interested in
   the notion of alpha-equivalence that is \emph{not} preserved by adding
   vacuous binders.) To answer this, we identify four conditions: {\it i)}
   given a free-variable function @{text "fv"} of type \mbox{@{text "\<beta> \<Rightarrow> atom
@@ -680,7 +680,7 @@
   \end{equation}
 
   It might be useful to consider some examples for how these definitions of alpha-equivalence
-  pan out in practise.
+  pan out in practice.
   For this consider the case of abstracting a set of variables over types (as in type-schemes). 
   We set @{text R} to be the equality and for @{text "fv(T)"} we define
 
@@ -784,8 +784,8 @@
   \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]}
+  @{thm (lhs) supp_abs(3)[where bs="as", no_vars]} & $=$ & @{thm (rhs) supp_abs(3)[where bs="as", no_vars]}\\
+  @{thm (lhs) supp_abs(2)[no_vars]} & $=$ & @{thm (rhs) supp_abs(2)[no_vars]}
   \end{tabular}
   \end{center}
   \end{thm}
@@ -809,7 +809,7 @@
 
   \noindent
   The second fact derives from the definition of permutations acting on pairs 
-  (see \eqref{permute}) and alpha-equivalence being equivariant 
+  \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.
   
@@ -1258,7 +1258,7 @@
   \end{center}
 
   \noindent
-  To see how these definitions work in practise, let us reconsider the term-constructors 
+  To see how these definitions work in practice, let us reconsider the term-constructors 
   @{text "Let"} and @{text "Let_rec"} from the example shown in \eqref{letrecs}. 
   For this specification we need to define three free-variable functions, namely
   @{text "fv\<^bsub>trm\<^esub>"}, @{text "fv\<^bsub>assn\<^esub>"} and @{text "fv\<^bsub>bn\<^esub>"}. They are as follows:
@@ -1737,7 +1737,7 @@
   $|$~@{text "bv3 (TVCKCons c cty tl) = (atom c)::(bv3 tl)"}\\
   \end{tabular}
   \end{boxedminipage}
-  \caption{The nominal datatype declaration for Core-Haskell. At the moment we
+  \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 
@@ -1917,7 +1917,7 @@
   Taking now the identity permutation @{text 0} for the permutations in \eqref{hyps},
   we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
   This completes the proof showing that the strong induction principle derives from
-  the weak induction principle. At the moment we can derive the difficult cases of 
+  the weak induction principle. For the moment we can derive the difficult cases of 
   the strong induction principles only by hand, but they are very schematically 
   so that with little effort we can even derive them for 
   Core-Haskell given in Figure~\ref{nominalcorehas}. 
@@ -2004,7 +2004,7 @@
   once. This extension has been tried out with the Core-Haskell
   term-calculus. For such general binders, we can also extend
   earlier work that derives strong induction principles which have the usual
-  variable convention already built in. At the moment we can do so only with manual help,
+  variable convention already built in. For the moment we can do so only with manual help,
   but future work will automate them completely.  The code underlying the presented
   extension will become part of the Isabelle distribution, but for the moment
   it can be downloaded from the Mercurial repository linked at