src/HOL/List.thy
changeset 49757 73ab6d4a9236
parent 49739 13aa6d8268ec
child 49808 418991ce7567
--- a/src/HOL/List.thy	Tue Oct 09 15:31:45 2012 +0200
+++ b/src/HOL/List.thy	Tue Oct 09 16:57:58 2012 +0200
@@ -5627,8 +5627,8 @@
   "Set.remove x (List.coset xs) = List.coset (List.insert x xs)"
   by (simp_all add: remove_def Compl_insert)
 
-lemma project_set [code]:
-  "Set.project P (set xs) = set (filter P xs)"
+lemma filter_set [code]:
+  "Set.filter P (set xs) = set (filter P xs)"
   by auto
 
 lemma image_set [code]: