src/HOL/Fun.thy
changeset 4830 bd73675adbed
parent 4648 f04da668581c
child 5305 513925de8962
     1.1 --- a/src/HOL/Fun.thy	Mon Apr 27 13:47:46 1998 +0200
     1.2 +++ b/src/HOL/Fun.thy	Mon Apr 27 16:45:11 1998 +0200
     1.3 @@ -12,15 +12,15 @@
     1.4                         (subset_refl,subset_trans,subset_antisym,psubset_eq)
     1.5  consts
     1.6  
     1.7 -  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
     1.8 -  inj_onto      :: ['a => 'b, 'a set] => bool
     1.9 -  inv           :: ('a => 'b) => ('b => 'a)
    1.10 +  inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
    1.11 +  inj_on      :: ['a => 'b, 'a set] => bool
    1.12 +  inv         :: ('a => 'b) => ('b => 'a)
    1.13  
    1.14  defs
    1.15  
    1.16 -  inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
    1.17 -  inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.18 -  surj_def      "surj f         == ! y. ? x. y=f(x)"
    1.19 -  inv_def       "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
    1.20 +  inj_def     "inj f          == ! x y. f(x)=f(y) --> x=y"
    1.21 +  inj_on_def  "inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
    1.22 +  surj_def    "surj f         == ! y. ? x. y=f(x)"
    1.23 +  inv_def     "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
    1.24  
    1.25  end