--- a/Nominal/Abs.thy	Mon Aug 16 17:39:16 2010 +0800
+++ b/Nominal/Abs.thy	Mon Aug 16 17:59:09 2010 +0800
@@ -533,7 +533,6 @@
 where
  "prod_alpha = prod_rel"
 
-
 lemma [quot_respect]:
   shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
   by auto
@@ -563,14 +562,6 @@
 
 
 
-
-
-
-
-
-
-
-
 section {* BELOW is stuff that may or may not be needed *}
 
 lemma supp_atom_image: