# HG changeset patch
# User huffman
# Date 1313445024 25200
# Node ID 786876687ef88dea9eb8e5ff1613c7f04021681b
# Parent  1e0414bda9af3cb4b6f4a55de4016b8a7245df4d
remove duplicate lemma disjoint_iff

diff -r 1e0414bda9af -r 786876687ef8 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Aug 15 14:29:17 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Aug 15 14:50:24 2011 -0700
@@ -272,9 +272,6 @@
 
 subsubsection {* Type @{typ "'a \<times> 'b"} *}
 
-lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
-  by auto (* TODO: move elsewhere *)
-
 instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
 begin
 
@@ -307,7 +304,7 @@
 next
   show "DIM('a \<times> 'b) = card (Basis :: ('a \<times> 'b) set)"
     unfolding dimension_prod_def Basis_prod_def
-    by (simp add: card_Un_disjoint disjoint_iff
+    by (simp add: card_Un_disjoint disjoint_iff_not_equal
       card_image inj_on_def dimension_def)
 next
   show "basis ` {..<DIM('a \<times> 'b)} = (Basis :: ('a \<times> 'b) set)"
diff -r 1e0414bda9af -r 786876687ef8 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Aug 15 14:29:17 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Aug 15 14:50:24 2011 -0700
@@ -590,7 +590,7 @@
 next
   show "DIM('a ^ 'b) = card (Basis :: ('a ^ 'b) set)"
     unfolding Basis_vec_def dimension_vec_def dimension_def
-    by (simp add: card_UN_disjoint [unfolded disjoint_iff]
+    by (simp add: card_UN_disjoint [unfolded disjoint_iff_not_equal]
       axis_eq_axis nonzero_Basis)
 next
   show "basis ` {..<DIM('a ^ 'b)} = (Basis :: ('a ^ 'b) set)"