src/HOL/Set.thy

   Bex1          :: "'a set => ('a => bool) => bool"      -- "bounded unique existential quantifiers"
   image         :: "('a => 'b) => 'a set => 'b set"      (infixr "`" 90)
   "op :"        :: "'a => 'a set => bool"                -- "membership"
 
 notation
-  "op :"  ("op :")
+  "op :"  ("op :") and
   "op :"  ("(_/ : _)" [50, 51] 50)
 
 local
 
 
 subsection {* Additional concrete syntax *}
 
 abbreviation
-  range :: "('a => 'b) => 'b set"             -- "of function"
+  range :: "('a => 'b) => 'b set" where -- "of function"
   "range f == f ` UNIV"
 
 abbreviation
-  "not_mem x A == ~ (x : A)"                  -- "non-membership"
+  "not_mem x A == ~ (x : A)" -- "non-membership"
 
 notation
-  not_mem  ("op ~:")
+  not_mem  ("op ~:") and
   not_mem  ("(_/ ~: _)" [50, 51] 50)
 
 notation (xsymbols)
-  "op Int"  (infixl "\<inter>" 70)
-  "op Un"  (infixl "\<union>" 65)
-  "op :"  ("op \<in>")
-  "op :"  ("(_/ \<in> _)" [50, 51] 50)
-  not_mem  ("op \<notin>")
-  not_mem  ("(_/ \<notin> _)" [50, 51] 50)
-  Union  ("\<Union>_" [90] 90)
+  "op Int"  (infixl "\<inter>" 70) and
+  "op Un"  (infixl "\<union>" 65) and
+  "op :"  ("op \<in>") and
+  "op :"  ("(_/ \<in> _)" [50, 51] 50) and
+  not_mem  ("op \<notin>") and
+  not_mem  ("(_/ \<notin> _)" [50, 51] 50) and
+  Union  ("\<Union>_" [90] 90) and
   Inter  ("\<Inter>_" [90] 90)
 
 notation (HTML output)
-  "op Int"  (infixl "\<inter>" 70)
-  "op Un"  (infixl "\<union>" 65)
-  "op :"  ("op \<in>")
-  "op :"  ("(_/ \<in> _)" [50, 51] 50)
-  not_mem  ("op \<notin>")
+  "op Int"  (infixl "\<inter>" 70) and
+  "op Un"  (infixl "\<union>" 65) and
+  "op :"  ("op \<in>") and
+  "op :"  ("(_/ \<in> _)" [50, 51] 50) and
+  not_mem  ("op \<notin>") and
   not_mem  ("(_/ \<notin> _)" [50, 51] 50)
 
 syntax
   "@Finset"     :: "args => 'a set"                       ("{(_)}")
   "@Coll"       :: "pttrn => bool => 'a set"              ("(1{_./ _})")

 instance set :: (type) ord
   subset_def:   "A <= B         == \<forall>x\<in>A. x \<in> B"
   psubset_def:  "A < B          == (A::'a set) <= B & ~ A=B" ..
 
 abbreviation
-  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "subset == less"
-  subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+
+abbreviation
+  subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "subset_eq == less_eq"
 
 notation (output)
-  subset  ("op <")
-  subset  ("(_/ < _)" [50, 51] 50)
-  subset_eq  ("op <=")
+  subset  ("op <") and
+  subset  ("(_/ < _)" [50, 51] 50) and
+  subset_eq  ("op <=") and
   subset_eq  ("(_/ <= _)" [50, 51] 50)
 
 notation (xsymbols)
-  subset  ("op \<subset>")
-  subset  ("(_/ \<subset> _)" [50, 51] 50)
-  subset_eq  ("op \<subseteq>")
+  subset  ("op \<subset>") and
+  subset  ("(_/ \<subset> _)" [50, 51] 50) and
+  subset_eq  ("op \<subseteq>") and
   subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
 
 notation (HTML output)
-  subset  ("op \<subset>")
-  subset  ("(_/ \<subset> _)" [50, 51] 50)
-  subset_eq  ("op \<subseteq>")
+  subset  ("op \<subset>") and
+  subset  ("(_/ \<subset> _)" [50, 51] 50) and
+  subset_eq  ("op \<subseteq>") and
   subset_eq  ("(_/ \<subseteq> _)" [50, 51] 50)
 
 abbreviation (input)
-  supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"    (infixl "\<supset>" 50)
+  supset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "\<supset>" 50) where
   "supset == greater"
-  supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "\<supseteq>" 50)
+
+abbreviation (input)
+  supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "\<supseteq>" 50) where
   "supset_eq == greater_eq"
 
 
 subsubsection "Bounded quantifiers"
 

  "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
  "\<forall>A\<subseteq>B. P"   =>  "ALL A. A \<subseteq> B --> P"
  "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
  "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"
 
+(* FIXME re-use version in Orderings.thy *)
 print_translation {*
 let
   fun
     all_tr' [Const ("_bound",_) $ Free (v,Type(T,_)), 
              Const("op -->",_) $ (Const ("less",_) $ (Const ("_bound",_) $ Free (v',_)) $ n ) $ P] =