diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Set.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -38,7 +38,7 @@
   "op :"        :: "'a => 'a set => bool"                -- "membership"
 
 notation
-  "op :"  ("op :")
+  "op :"  ("op :") and
   "op :"  ("(_/ : _)" [50, 51] 50)
 
 local
@@ -47,32 +47,32 @@
 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
@@ -149,33 +149,37 @@
   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"
 
 
@@ -216,6 +220,7 @@
  "\<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