diff -r bec099d10563 -r e26e933efba0 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Mon Jan 09 10:12:46 2012 +0000
+++ b/LMCS-Paper/Paper.thy	Mon Jan 09 10:45:12 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},