# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277305183 -3600
# Node ID f170ee51eed2f6a7273f7f21aa375287b0f8a5a5
# Parent  8728f7990f6d23368787655b2ad76775e6747977
some slight polishing on the paper

diff -r 8728f7990f6d -r f170ee51eed2 Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Jun 23 15:40:00 2010 +0100
+++ b/Paper/Paper.thy	Wed Jun 23 15:59:43 2010 +0100
@@ -29,11 +29,11 @@
   fv ("fv'(_')" [100] 100) and
   equal ("=") and
   alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
-  Abs ("[_]\<^raw:$\!$>\<^bsub>set\<^esub>._" [20, 101] 999) and
-  Abs_lst ("[_]\<^raw:$\!$>\<^bsub>list\<^esub>._") and
-  Abs_dist ("[_]\<^raw:$\!$>\<^bsub>#list\<^esub>._") and
-  Abs_res ("[_]\<^raw:$\!$>\<^bsub>res\<^esub>._") and
-  Abs_print ("_\<^raw:$\!$>\<^bsub>set\<^esub>._") and
+  Abs ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
+  Abs_lst ("[_]\<^bsub>list\<^esub>._") and
+  Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
+  Abs_res ("[_]\<^bsub>res\<^esub>._") and
+  Abs_print ("_\<^bsub>set\<^esub>._") and
   Cons ("_::_" [78,77] 73) and
   supp_gen ("aux _" [1000] 10) and
   alpha_bn ("_ \<approx>bn _")
@@ -115,9 +115,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{Leroy92} is incorrect (it omits a side-condition). A related
-  notion of alpha-equivalence that allows vacuous binders, there called weakening 
-  of contexts, is defined in for the $\Pi\Sigma$-calculus \cite{Altenkirch10}.
+  Leroy in \cite{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