# HG changeset patch
# User nipkow
# Date 1355761161 -3600
# Node ID fbb973a5310662b1682dd184a7ba65d4944968fa
# Parent  8ccffe44d19344ee1c60be6b6de90430cec7204e
made element and subset relations non-associative (just like all orderings)

diff -r 8ccffe44d193 -r fbb973a53106 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Dec 17 15:18:39 2012 +0100
+++ b/src/HOL/Set.thy	Mon Dec 17 17:19:21 2012 +0100
@@ -18,26 +18,26 @@
 
 notation
   member  ("op :") and
-  member  ("(_/ : _)" [50, 51] 50)
+  member  ("(_/ : _)" [51, 51] 50)
 
 abbreviation not_member where
   "not_member x A \<equiv> ~ (x : A)" -- "non-membership"
 
 notation
   not_member  ("op ~:") and
-  not_member  ("(_/ ~: _)" [50, 51] 50)
+  not_member  ("(_/ ~: _)" [51, 51] 50)
 
 notation (xsymbols)
   member      ("op \<in>") and
-  member      ("(_/ \<in> _)" [50, 51] 50) and
+  member      ("(_/ \<in> _)" [51, 51] 50) and
   not_member  ("op \<notin>") and
-  not_member  ("(_/ \<notin> _)" [50, 51] 50)
+  not_member  ("(_/ \<notin> _)" [51, 51] 50)
 
 notation (HTML output)
   member      ("op \<in>") and
-  member      ("(_/ \<in> _)" [50, 51] 50) and
+  member      ("(_/ \<in> _)" [51, 51] 50) and
   not_member  ("op \<notin>") and
-  not_member  ("(_/ \<notin> _)" [50, 51] 50)
+  not_member  ("(_/ \<notin> _)" [51, 51] 50)
 
 
 text {* Set comprehensions *}
@@ -156,21 +156,21 @@
 
 notation (output)
   subset  ("op <") and
-  subset  ("(_/ < _)" [50, 51] 50) and
+  subset  ("(_/ < _)" [51, 51] 50) and
   subset_eq  ("op <=") and
-  subset_eq  ("(_/ <= _)" [50, 51] 50)
+  subset_eq  ("(_/ <= _)" [51, 51] 50)
 
 notation (xsymbols)
   subset  ("op \<subset>") and
-  subset  ("(_/ \<subset> _)" [50, 51] 50) and
+  subset  ("(_/ \<subset> _)" [51, 51] 50) and
   subset_eq  ("op \<subseteq>") and
-  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
+  subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
 
 notation (HTML output)
   subset  ("op \<subset>") and
-  subset  ("(_/ \<subset> _)" [50, 51] 50) and
+  subset  ("(_/ \<subset> _)" [51, 51] 50) and
   subset_eq  ("op \<subseteq>") and
-  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
+  subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
 
 abbreviation (input)
   supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
@@ -182,9 +182,9 @@
 
 notation (xsymbols)
   supset  ("op \<supset>") and
-  supset  ("(_/ \<supset> _)" [50, 51] 50) and
+  supset  ("(_/ \<supset> _)" [51, 51] 50) and
   supset_eq  ("op \<supseteq>") and
-  supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
+  supset_eq  ("(_/ \<supseteq> _)" [51, 51] 50)
 
 definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   -- "bounded universal quantifiers"