# 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 \Misc\ - -abbreviation (input) transP :: "('a \ 'a \ bool) \ bool" - where "transP r \ trans {(x, y). r x y}" (* FIXME drop *) - end