prefer existing logical constant over abbreviation
authorhaftmann
Wed Dec 21 21:26:26 2016 +0100 (2016-12-21)
changeset 646335ebcf6c525f1
parent 64632 9df24b8b6c0a
child 64634 5bd30359e46e
prefer existing logical constant over abbreviation
NEWS
src/HOL/Relation.thy
     1.1 --- a/NEWS	Wed Dec 21 21:26:26 2016 +0100
     1.2 +++ b/NEWS	Wed Dec 21 21:26:26 2016 +0100
     1.3 @@ -19,6 +19,8 @@
     1.4  * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Dropped abbreviation transP; use constant transp instead.
     1.8 +
     1.9  * Swapped orientation of congruence rules mod_add_left_eq,
    1.10  mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
    1.11  mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
     2.1 --- a/src/HOL/Relation.thy	Wed Dec 21 21:26:26 2016 +0100
     2.2 +++ b/src/HOL/Relation.thy	Wed Dec 21 21:26:26 2016 +0100
     2.3 @@ -1149,9 +1149,4 @@
     2.4      (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
     2.5        cong: if_cong)
     2.6  
     2.7 -text \<open>Misc\<close>
     2.8 -
     2.9 -abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    2.10 -  where "transP r \<equiv> trans {(x, y). r x y}"  (* FIXME drop *)
    2.11 -
    2.12  end