
diff -r d81fb5b46a5c -r f6ce08859d4c src/HOL/Set.thy
--- 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 = {}"
 




