added translation to fix critical pair between abbreviations for surj and ~=
authornipkow
Thu, 07 Jul 2011 21:53:53 +0200
changeset 43705 8e421a529a48
parent 43694 93dcfcf91484
child 43706 4068e95f1e43
added translation to fix critical pair between abbreviations for surj and ~=
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"