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