diff -r 7645e18e8b19 -r 80db544a37ea Nominal/Abs.thy --- 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: