src/HOL/Relation.thy
changeset 64633 5ebcf6c525f1
parent 64632 9df24b8b6c0a
child 64634 5bd30359e46e
     1.1 --- a/src/HOL/Relation.thy	Wed Dec 21 21:26:26 2016 +0100
     1.2 +++ b/src/HOL/Relation.thy	Wed Dec 21 21:26:26 2016 +0100
     1.3 @@ -1149,9 +1149,4 @@
     1.4      (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
     1.5        cong: if_cong)
     1.6  
     1.7 -text \<open>Misc\<close>
     1.8 -
     1.9 -abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
    1.10 -  where "transP r \<equiv> trans {(x, y). r x y}"  (* FIXME drop *)
    1.11 -
    1.12  end