src/HOL/Set.thy
changeset 8005 b64d86018785
parent 7358 9e95b846ad42
child 8148 5ef0b624aadb
--- a/src/HOL/Set.thy	Thu Nov 11 10:24:14 1999 +0100
+++ b/src/HOL/Set.thy	Thu Nov 11 10:25:17 1999 +0100
@@ -35,7 +35,7 @@
   Pow           :: 'a set => 'a set set                 (*powerset*)
   range         :: ('a => 'b) => 'b set                 (*of function*)
   Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
-  "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
+  "image"       :: ['a => 'b, 'a set] => ('b set)   (infixr "``" 90)
   (*membership*)
   "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)