diff -r f10b141078e7 -r 09be06943252 src/HOL/Library/SetsAndFunctions.thy --- a/src/HOL/Library/SetsAndFunctions.thy Tue May 16 21:32:56 2006 +0200 +++ b/src/HOL/Library/SetsAndFunctions.thy Tue May 16 21:33:01 2006 +0200 @@ -58,7 +58,7 @@ elt_set_times :: "'a::times => 'a set => 'a set" (infixl "*o" 80) "a *o B == {c. EX b:B. c = a * b}" -abbreviation (inout) +abbreviation (input) elt_set_eq :: "'a => 'a set => bool" (infix "=o" 50) "x =o A == x : A"