diff -r 12378df46752 -r 9dd394c866fc src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Oct 01 23:26:31 2015 +0200
+++ b/src/HOL/Set.thy	Fri Oct 02 15:07:41 2015 +0100
@@ -1931,6 +1931,8 @@
 
 text \<open>Misc\<close>
 
+definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
+
 hide_const (open) member not_member
 
 lemmas equalityI = subset_antisym