--- 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.
--- 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