--- a/NEWS Wed Dec 21 21:26:26 2016 +0100
+++ b/NEWS Wed Dec 21 21:26:26 2016 +0100
@@ -19,6 +19,8 @@
* Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
INCOMPATIBILITY.
+* Dropped abbreviation transP; use constant transp instead.
+
* Swapped orientation of congruence rules mod_add_left_eq,
mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
--- a/src/HOL/Relation.thy Wed Dec 21 21:26:26 2016 +0100
+++ b/src/HOL/Relation.thy Wed Dec 21 21:26:26 2016 +0100
@@ -1149,9 +1149,4 @@
(auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
cong: if_cong)
-text \<open>Misc\<close>
-
-abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
- where "transP r \<equiv> trans {(x, y). r x y}" (* FIXME drop *)
-
end