| changeset 7877 | e5e019d60f71 |
| parent 7845 | 3561e0da35b8 |
| child 7914 | 5bfde29f1dbb |
--- a/src/HOL/equalities.ML Mon Oct 18 15:16:10 1999 +0200 +++ b/src/HOL/equalities.ML Mon Oct 18 15:17:35 1999 +0200 @@ -201,6 +201,10 @@ by (blast_tac (claset() addSEs [equalityCE]) 1); qed "disjoint_eq_subset_Compl"; +Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)"; +by (Blast_tac 1); +qed "disjoint_iff_not_equal"; + Goal "UNIV Int B = B"; by (Blast_tac 1); qed "Int_UNIV_left";