--- a/Nominal/Parser.thy	Tue Apr 20 11:29:00 2010 +0200
+++ b/Nominal/Parser.thy	Tue Apr 20 18:24:50 2010 +0200
@@ -296,14 +296,19 @@
 
 Parser.thy/raw_nominal_decls
   1) define the raw datatype
-  2) define the raw binding functions
+  2) define the raw binding functions 
+
 Perm.thy/define_raw_perms
-  3) define permutations of the raw datatype and show that raw type is in the pt typeclass
+  3) define permutations of the raw datatype and show that the raw type is 
+     in the pt typeclass
+      
 Lift.thy/define_fv_alpha_export, Fv.thy/define_fv & define_alpha
   4) define fv and fv_bn
   5) define alpha and alpha_bn
+
 Perm.thy/distinct_rel
   6) prove alpha_distincts (C1 x \<notsimeq> C2 y ...)             (Proof by cases; simp)
+
 Tacs.thy/build_rel_inj
   6) prove alpha_eq_iff    (C1 x = C2 y \<leftrightarrow> P x y ...)
      (left-to-right by intro rule, right-to-left by cases; simp)