
diff -r 3ca3bc795908 -r eb5d493a9e03 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed May 04 10:19:01 2016 +0200
+++ b/src/HOL/Set.thy	Mon May 09 16:02:23 2016 +0100
@@ -1905,13 +1905,16 @@
 
 definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
 
+lemma pairwise_subset: "\<lbrakk>pairwise P S; T \<subseteq> S\<rbrakk> \<Longrightarrow> pairwise P T"
+  by (force simp: pairwise_def)
+
 definition disjnt where "disjnt A B \<equiv> A \<inter> B = {}"
 
-lemma pairwise_disjoint_empty [simp]: "pairwise disjnt {}"
-  by (simp add: pairwise_def disjnt_def)
-
-lemma pairwise_disjoint_singleton [simp]: "pairwise disjnt {A}"
-  by (simp add: pairwise_def disjnt_def)
+lemma pairwise_empty [simp]: "pairwise P {}"
+  by (simp add: pairwise_def)
+
+lemma pairwise_singleton [simp]: "pairwise P {A}"
+  by (simp add: pairwise_def)
 
 hide_const (open) member not_member
 




