# HG changeset patch
# User paulson
# Date 940252655 -7200
# Node ID e5e019d60f71faccb544587086d4bbb2d7eb7402
# Parent  1b3b683c092e5d4c9af8484383ee9cdb9c5c8e28
new thm disjoint_iff_not_equal

diff -r 1b3b683c092e -r e5e019d60f71 src/HOL/equalities.ML
--- 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";