src/HOL/Fun.thy

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