--- a/src/HOL/Set.thy Wed Sep 21 16:59:51 2016 +0100
+++ b/src/HOL/Set.thy Thu Sep 22 15:44:47 2016 +0100
@@ -1852,6 +1852,9 @@
lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T"
by (force simp: pairwise_def)
+lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
+ by (auto simp: pairwise_def)
+
definition disjnt :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
where "disjnt A B \<longleftrightarrow> A \<inter> B = {}"