--- a/LMCS-Paper/Paper.thy	Thu Dec 29 18:05:13 2011 +0000
+++ b/LMCS-Paper/Paper.thy	Mon Jan 02 16:13:16 2012 +0000
@@ -114,7 +114,11 @@
   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
   binders by iterating single binders, this leads to a rather clumsy
-  formalisation of W. The need of iterating single binders is also one reason
+  formalisation of W. 
+
+  {\bf add example about W}
+
+  The need of iterating single binders is also one reason
   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},