1.1 --- a/src/HOL/Fun.thy	Wed Jul 06 23:11:59 2011 +0200
     1.2 +++ b/src/HOL/Fun.thy	Thu Jul 07 21:53:53 2011 +0200
     1.3 @@ -148,6 +148,10 @@
     1.4  abbreviation
     1.5    "bij f \<equiv> bij_betw f UNIV UNIV"
     1.6  
     1.7 +text{* The negated case: *}
     1.8 +translations
     1.9 +"\<not> CONST surj f" <= "CONST range f \<noteq> CONST UNIV"
    1.10 +
    1.11  lemma injI:
    1.12    assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
    1.13    shows "inj f"