# HG changeset patch
# User nipkow
# Date 1310120326 -7200
# Node ID 4068e95f1e43ad9d2dab974fcad8b628518cc11c
# Parent  47b0be18ccbea838adc69c416049f0a3eff94b9e# Parent  8e421a529a487ad1e34a8c5a12c842e1d5715c99
merged

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