# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1283518389 -28800
# Node ID 217149972715efc3dad6eddf666cfb717531160b
# Parent  937b6088a3a069c1ebe82583a50e1ec81e6157af
removed lemma finite_set (already in simpset)

diff -r 937b6088a3a0 -r 217149972715 Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Fri Sep 03 20:48:45 2010 +0800
+++ b/Nominal-General/Nominal2_Supp.thy	Fri Sep 03 20:53:09 2010 +0800
@@ -548,7 +548,7 @@
   shows "supp (set xs) = supp xs"
 apply(induct xs)
 apply(simp add: supp_set_empty supp_Nil)
-apply(simp add: supp_Cons finite_set supp_of_fin_insert)
+apply(simp add: supp_Cons supp_of_fin_insert)
 done
 
 end