| changeset 19656 | 09be06943252 | 
| parent 19380 | b808efaa5828 | 
| child 19736 | d8d0f8f51d69 | 
--- 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"