diff -r 8f4810b9d9d1 -r c8caefb20564 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Feb 18 20:08:21 2018 +0100
+++ b/src/HOL/Set.thy	Mon Feb 19 16:44:45 2018 +0000
@@ -1849,7 +1849,7 @@
 definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
 
-lemma pairwiseI:
+lemma pairwiseI [intro?]:
   "pairwise R S" if "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y"
   using that by (simp add: pairwise_def)
 
@@ -1871,8 +1871,8 @@
 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)
+lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y; B \<subseteq> A\<rbrakk> \<Longrightarrow> pairwise Q B"
+  by (fastforce simp: pairwise_def)
 
 lemma pairwise_imageI:
   "pairwise P (f ` A)"