src/HOL/Set.thy
changeset 1273 6960ec882bca
parent 1068 e0f2dffab506
child 1370 7361ac9b024d
equal deleted inserted replaced
1272:dd877dc7c1f4 1273:6960ec882bca
    98   image_def     "f``A           == {y. ? x:A. y=f(x)}"
    98   image_def     "f``A           == {y. ? x:A. y=f(x)}"
    99   inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
    99   inj_def       "inj(f)         == ! x y. f(x)=f(y) --> x=y"
   100   inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
   100   inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
   101   surj_def      "surj(f)        == ! y. ? x. y=f(x)"
   101   surj_def      "surj(f)        == ! y. ? x. y=f(x)"
   102 
   102 
       
   103 (* start 8bit 1 *)
       
   104 (* end 8bit 1 *)
       
   105 
   103 end
   106 end
   104 
   107 
   105 ML
   108 ML
   106 
   109 
   107 local
   110 local