src/HOL/Set.thy
changeset 10832 e33b47e4246d
parent 10131 546686f0a6fb
child 10985 65a8a0e2d55b
     1.1 --- a/src/HOL/Set.thy	Tue Jan 09 15:18:07 2001 +0100
     1.2 +++ b/src/HOL/Set.thy	Tue Jan 09 15:22:13 2001 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4    Union, Inter  :: (('a set) set) => 'a set             (*of a set*)
     1.5    Pow           :: 'a set => 'a set set                 (*powerset*)
     1.6    Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
     1.7 -  "image"       :: ['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  
    1.12 @@ -70,7 +70,7 @@
    1.13    "_Bex"        :: [pttrn, 'a set, bool] => bool      ("(3? _:_./ _)" [0, 0, 10] 10)
    1.14  
    1.15  translations
    1.16 -  "range f"     == "f``UNIV"
    1.17 +  "range f"     == "f`UNIV"
    1.18    "x ~: y"      == "~ (x : y)"
    1.19    "{x, xs}"     == "insert x {xs}"
    1.20    "{x}"         == "insert x {}"
    1.21 @@ -145,7 +145,7 @@
    1.22    empty_def     "{}             == {x. False}"
    1.23    UNIV_def      "UNIV           == {x. True}"
    1.24    insert_def    "insert a B     == {x. x=a} Un B"
    1.25 -  image_def     "f``A           == {y. ? x:A. y=f(x)}"
    1.26 +  image_def     "f`A           == {y. ? x:A. y=f(x)}"
    1.27  
    1.28  
    1.29  end