# HG changeset patch
# User nipkow
# Date 1310068433 -7200
# Node ID 8e421a529a487ad1e34a8c5a12c842e1d5715c99
# Parent  93dcfcf914848dea333e530761dd616c2c5c1744
added translation to fix critical pair between abbreviations for surj and ~=

diff -r 93dcfcf91484 -r 8e421a529a48 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"