| changeset 46147 | 2c4d8de91c4c |
| parent 45969 | 562e99c3d316 |
| child 46305 | 8ea02e499d53 |
--- a/src/HOL/Library/List_Cset.thy Fri Jan 06 21:48:45 2012 +0100 +++ b/src/HOL/Library/List_Cset.thy Fri Jan 06 22:16:01 2012 +0100 @@ -72,7 +72,7 @@ lemma filter_set [code]: "Cset.filter P (Cset.set xs) = Cset.set (List.filter P xs)" - by (simp add: Cset.set_def project_set) + by (simp add: Cset.set_def) lemma forall_set [code]: "Cset.forall P (Cset.set xs) \<longleftrightarrow> list_all P xs"