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