diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -52,14 +52,15 @@
   set_one: "1::('a::one)set == {1}"
 
 definition
-  elt_set_plus :: "'a::plus => 'a set => 'a set"    (infixl "+o" 70)
+  elt_set_plus :: "'a::plus => 'a set => 'a set"  (infixl "+o" 70) where
   "a +o B = {c. EX b:B. c = a + b}"
 
-  elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80)
+definition
+  elt_set_times :: "'a::times => 'a set => 'a set"  (infixl "*o" 80) where
   "a *o B = {c. EX b:B. c = a * b}"
 
 abbreviation (input)
-  elt_set_eq :: "'a => 'a set => bool"      (infix "=o" 50)
+  elt_set_eq :: "'a => 'a set => bool"  (infix "=o" 50) where
   "x =o A == x : A"
 
 instance "fun" :: (type,semigroup_add)semigroup_add