src/HOL/Set.thy
changeset 1883 00b4b6992945
parent 1674 33aff4d854e4
child 1962 e60a230da179
     1.1 --- a/src/HOL/Set.thy	Fri Jul 26 12:16:17 1996 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Jul 26 12:17:04 1996 +0200
     1.3 @@ -60,6 +60,7 @@
     1.4  
     1.5  translations
     1.6    "UNIV"        == "Compl {}"
     1.7 +  "range(f)"    == "f``UNIV"
     1.8    "x ~: y"      == "~ (x : y)"
     1.9    "{x, xs}"     == "insert x {xs}"
    1.10    "{x}"         == "insert x {}"
    1.11 @@ -97,7 +98,6 @@
    1.12    Pow_def       "Pow(A)         == {B. B <= A}"
    1.13    empty_def     "{}             == {x. False}"
    1.14    insert_def    "insert a B     == {x.x=a} Un B"
    1.15 -  range_def     "range(f)       == {y. ? x. y=f(x)}"
    1.16    image_def     "f``A           == {y. ? x:A. y=f(x)}"
    1.17    inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
    1.18    inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"