merged
authornipkow
Fri, 08 Jul 2011 12:18:46 +0200
changeset 43706 4068e95f1e43
parent 43704 47b0be18ccbe (current diff)
parent 43705 8e421a529a48 (diff)
child 43707 8a61f2441b62
merged
--- 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"