1.1 --- a/src/HOL/Fun.thy	Thu Jul 07 23:33:14 2011 +0200
     1.2 +++ b/src/HOL/Fun.thy	Fri Jul 08 12:18:46 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"