new thm disjoint_iff_not_equal

--- 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";