# HG changeset patch
# User haftmann
# Date 1489150055 -3600
# Node ID 53675f36820d2e76e117836c99e807bcca95b068
# Parent  a8dfa258bf93e26d5450d49da30650f4faedac28
restored surj as output abbreviation, amending 6af79184bef3

diff -r a8dfa258bf93 -r 53675f36820d NEWS
--- a/NEWS	Thu Mar 09 21:55:02 2017 +0100
+++ b/NEWS	Fri Mar 10 13:47:35 2017 +0100
@@ -48,6 +48,9 @@
 
 *** HOL ***
 
+* Constant "surj" is a full input/output abbreviation (again).
+Minor INCOMPATIBILITY.
+
 * Theory Library/FinFun has been moved to AFP (again).  INCOMPATIBILITY.
 
 * Some old and rarely used ASCII replacement syntax has been removed.
diff -r a8dfa258bf93 -r 53675f36820d src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Mar 09 21:55:02 2017 +0100
+++ b/src/HOL/Fun.thy	Fri Mar 10 13:47:35 2017 +0100
@@ -148,12 +148,17 @@
   the entire domain type.
 \<close>
 
-abbreviation "inj f \<equiv> inj_on f UNIV"
+abbreviation inj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  where "inj f \<equiv> inj_on f UNIV"
 
-abbreviation (input) surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
+abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
   where "surj f \<equiv> range f = UNIV"
 
-abbreviation "bij f \<equiv> bij_betw f UNIV UNIV"
+translations -- \<open>The negated case:\<close>
+  "\<not> CONST surj f" \<leftharpoondown> "CONST range f \<noteq> CONST UNIV"
+
+abbreviation bij :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
+  where "bij f \<equiv> bij_betw f UNIV UNIV"
 
 lemma inj_def: "inj f \<longleftrightarrow> (\<forall>x y. f x = f y \<longrightarrow> x = y)"
   unfolding inj_on_def by blast