src/HOL/Library/RBT_Set.thy
changeset 49757 73ab6d4a9236
parent 48623 bea613f2543d
child 49758 718f10c8bbfc
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Oct 09 15:31:45 2012 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Oct 09 16:57:58 2012 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4    "UNIV = UNIV" ..
     1.5  
     1.6  lemma [code, code del]:
     1.7 -  "Set.project = Set.project" ..
     1.8 +  "Set.filter = Set.filter" ..
     1.9  
    1.10  lemma [code, code del]:
    1.11    "image = image" ..
    1.12 @@ -602,8 +602,8 @@
    1.13    "A - Coset t = rbt_filter (\<lambda>k. k \<in> A) t"
    1.14  by (simp add: inter_Set[simplified Int_commute])
    1.15  
    1.16 -lemma project_Set [code]:
    1.17 -  "Set.project P (Set t) = (rbt_filter P t)"
    1.18 +lemma filter_Set [code]:
    1.19 +  "Set.filter P (Set t) = (rbt_filter P t)"
    1.20  by (auto simp add: project_filter finite_filter_rbt_filter)
    1.21  
    1.22  lemma image_Set [code]: