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)