src/HOL/Library/SetsAndFunctions.thy
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"