src/HOL/Set.thy
changeset 2912 3fac3e8d5d3e
parent 2684 9781d63ef063
child 2965 afbda7e26f15
     1.1 --- a/src/HOL/Set.thy	Fri Apr 04 16:27:39 1997 +0200
     1.2 +++ b/src/HOL/Set.thy	Fri Apr 04 16:33:28 1997 +0200
     1.3 @@ -32,8 +32,6 @@
     1.4    Pow           :: 'a set => 'a set set                 (*powerset*)
     1.5    range         :: ('a => 'b) => 'b set                 (*of function*)
     1.6    Ball, Bex     :: ['a set, 'a => bool] => bool         (*bounded quantifiers*)
     1.7 -  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
     1.8 -  inj_onto      :: ['a => 'b, 'a set] => bool
     1.9    "``"          :: ['a => 'b, 'a set] => ('b set)   (infixr 90)
    1.10    (*membership*)
    1.11    "op :"        :: ['a, 'a set] => bool             ("(_/ : _)" [50, 51] 50)
    1.12 @@ -149,9 +147,6 @@
    1.13    empty_def     "{}             == {x. False}"
    1.14    insert_def    "insert a B     == {x.x=a} Un B"
    1.15    image_def     "f``A           == {y. ? x:A. y=f(x)}"
    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  
    1.20  end
    1.21