Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed lemma finite_set (already in simpset)
authorChristian Urban <urbanc@in.tum.de>
Fri, 03 Sep 2010 20:53:09 +0800
changeset 2463 217149972715
parent 2462 937b6088a3a0
child 2464 f4eba60cbd69
removed lemma finite_set (already in simpset)
Nominal-General/Nominal2_Supp.thy file | annotate | diff | comparison | revisions 
--- 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
nominal2