src/HOL/Fun.thy
changeset 19363 667b5ea637dd
parent 19323 ec5cd5b1804c
child 19536 1a3a3cf8b4fa
     1.1 --- a/src/HOL/Fun.thy	Sat Apr 08 22:12:02 2006 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sat Apr 08 22:51:06 2006 +0200
     1.3 @@ -59,19 +59,19 @@
     1.4  
     1.5  constdefs
     1.6    inj_on :: "['a => 'b, 'a set] => bool"         (*injective*)
     1.7 -    "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     1.8 +  "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
     1.9  
    1.10  text{*A common special case: functions injective over the entire domain type.*}
    1.11  
    1.12 -abbreviation (output)
    1.13 -  "inj f = inj_on f UNIV"
    1.14 +abbreviation
    1.15 +  "inj f == inj_on f UNIV"
    1.16  
    1.17  constdefs
    1.18    surj :: "('a => 'b) => bool"                   (*surjective*)
    1.19 -    "surj f == ! y. ? x. y=f(x)"
    1.20 +  "surj f == ! y. ? x. y=f(x)"
    1.21  
    1.22    bij :: "('a => 'b) => bool"                    (*bijective*)
    1.23 -    "bij f == inj f & surj f"
    1.24 +  "bij f == inj f & surj f"
    1.25  
    1.26  
    1.27