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