| changeset 61306 | 9dd394c866fc |
| parent 60758 | d8d85a8172b5 |
| child 61378 | 3e04c9ca001a |
--- 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