# HG changeset patch
# User haftmann
# Date 1482351986 -3600
# Node ID 5ebcf6c525f1fa965b3771853e59773197cd5fe7
# Parent  9df24b8b6c0aaa3a1130dc4cf6a4dc88e692ed00
prefer existing logical constant over abbreviation

diff -r 9df24b8b6c0a -r 5ebcf6c525f1 NEWS
--- 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,
diff -r 9df24b8b6c0a -r 5ebcf6c525f1 src/HOL/Relation.thy
--- 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