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