Mercurial Mercurial > repos > Old_HOL / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
equalities.ML
changeset 205 ccbbe1264c0f
parent 171 16c4ea954511 
--- a/equalities.ML	Sun Jan 29 14:02:17 1995 +0100
+++ b/equalities.ML	Mon Jan 30 16:32:32 1995 +0100
@@ -62,7 +62,7 @@
 by (fast_tac eq_cs 1);
 qed "Int_empty_right";
 
-goal Set.thy "(A Un B) Int C  =  (A Int C) Un (B Int C)";
+goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
 by (fast_tac eq_cs 1);
 qed "Int_Un_distrib";
 
@@ -113,6 +113,10 @@
 by (fast_tac eq_cs 1);
 qed "subset_insert_iff";
 
+goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
+by (fast_tac (eq_cs addEs [equalityCE]) 1);
+qed "Un_empty";
+
 (** Simple properties of Compl -- complement of a set **)
 
 goal Set.thy "A Int Compl(A) = {}";
@@ -322,7 +326,7 @@
 val set_ss = set_ss addsimps
   [in_empty,in_insert,insert_subset,
    Int_absorb,Int_empty_left,Int_empty_right,
-   Un_absorb,Un_empty_left,Un_empty_right,
+   Un_absorb,Un_empty_left,Un_empty_right,Un_empty,
    UN1_constant,image_empty,
    Compl_disjoint,double_complement,
    Union_empty,Union_insert,empty_subsetI,subset_refl,
Old_HOL