| changeset 18423 | d7859164447f |
| parent 18413 | 50c0c118e96d |
| child 18447 | da548623916a |
--- a/src/HOL/Set.thy Fri Dec 16 16:00:58 2005 +0100 +++ b/src/HOL/Set.thy Fri Dec 16 16:59:32 2005 +0100 @@ -1120,7 +1120,10 @@ by (unfold psubset_def) blast lemma Collect_empty_eq [simp]: "(Collect P = {}) = (\<forall>x. \<not> P x)" - by auto +by blast + +lemma empty_Collect_eq [simp]: "({} = Collect P) = (\<forall>x. \<not> P x)" +by blast lemma Collect_neg_eq: "{x. \<not> P x} = - {x. P x}" by blast