made element and subset relations non-associative (just like all orderings)
authornipkow
Mon Dec 17 17:19:21 2012 +0100 (2012-12-17)
changeset 50580fbb973a53106
parent 50579 8ccffe44d193
child 50581 0eaefd4306d7
made element and subset relations non-associative (just like all orderings)
src/HOL/Set.thy
     1.1 --- a/src/HOL/Set.thy	Mon Dec 17 15:18:39 2012 +0100
     1.2 +++ b/src/HOL/Set.thy	Mon Dec 17 17:19:21 2012 +0100
     1.3 @@ -18,26 +18,26 @@
     1.4  
     1.5  notation
     1.6    member  ("op :") and
     1.7 -  member  ("(_/ : _)" [50, 51] 50)
     1.8 +  member  ("(_/ : _)" [51, 51] 50)
     1.9  
    1.10  abbreviation not_member where
    1.11    "not_member x A \<equiv> ~ (x : A)" -- "non-membership"
    1.12  
    1.13  notation
    1.14    not_member  ("op ~:") and
    1.15 -  not_member  ("(_/ ~: _)" [50, 51] 50)
    1.16 +  not_member  ("(_/ ~: _)" [51, 51] 50)
    1.17  
    1.18  notation (xsymbols)
    1.19    member      ("op \<in>") and
    1.20 -  member      ("(_/ \<in> _)" [50, 51] 50) and
    1.21 +  member      ("(_/ \<in> _)" [51, 51] 50) and
    1.22    not_member  ("op \<notin>") and
    1.23 -  not_member  ("(_/ \<notin> _)" [50, 51] 50)
    1.24 +  not_member  ("(_/ \<notin> _)" [51, 51] 50)
    1.25  
    1.26  notation (HTML output)
    1.27    member      ("op \<in>") and
    1.28 -  member      ("(_/ \<in> _)" [50, 51] 50) and
    1.29 +  member      ("(_/ \<in> _)" [51, 51] 50) and
    1.30    not_member  ("op \<notin>") and
    1.31 -  not_member  ("(_/ \<notin> _)" [50, 51] 50)
    1.32 +  not_member  ("(_/ \<notin> _)" [51, 51] 50)
    1.33  
    1.34  
    1.35  text {* Set comprehensions *}
    1.36 @@ -156,21 +156,21 @@
    1.37  
    1.38  notation (output)
    1.39    subset  ("op <") and
    1.40 -  subset  ("(_/ < _)" [50, 51] 50) and
    1.41 +  subset  ("(_/ < _)" [51, 51] 50) and
    1.42    subset_eq  ("op <=") and
    1.43 -  subset_eq  ("(_/ <= _)" [50, 51] 50)
    1.44 +  subset_eq  ("(_/ <= _)" [51, 51] 50)
    1.45  
    1.46  notation (xsymbols)
    1.47    subset  ("op \<subset>") and
    1.48 -  subset  ("(_/ \<subset> _)" [50, 51] 50) and
    1.49 +  subset  ("(_/ \<subset> _)" [51, 51] 50) and
    1.50    subset_eq  ("op \<subseteq>") and
    1.51 -  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
    1.52 +  subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
    1.53  
    1.54  notation (HTML output)
    1.55    subset  ("op \<subset>") and
    1.56 -  subset  ("(_/ \<subset> _)" [50, 51] 50) and
    1.57 +  subset  ("(_/ \<subset> _)" [51, 51] 50) and
    1.58    subset_eq  ("op \<subseteq>") and
    1.59 -  subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
    1.60 +  subset_eq  ("(_/ \<subseteq> _)" [51, 51] 50)
    1.61  
    1.62  abbreviation (input)
    1.63    supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    1.64 @@ -182,9 +182,9 @@
    1.65  
    1.66  notation (xsymbols)
    1.67    supset  ("op \<supset>") and
    1.68 -  supset  ("(_/ \<supset> _)" [50, 51] 50) and
    1.69 +  supset  ("(_/ \<supset> _)" [51, 51] 50) and
    1.70    supset_eq  ("op \<supseteq>") and
    1.71 -  supset_eq  ("(_/ \<supseteq> _)" [50, 51] 50)
    1.72 +  supset_eq  ("(_/ \<supseteq> _)" [51, 51] 50)
    1.73  
    1.74  definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
    1.75    "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   -- "bounded universal quantifiers"