src/HOL/Relation.thy
changeset 64632 9df24b8b6c0a
parent 64584 142ac30b68fe
child 64633 5ebcf6c525f1
--- a/src/HOL/Relation.thy	Wed Dec 21 21:26:25 2016 +0100
+++ b/src/HOL/Relation.thy	Wed Dec 21 21:26:26 2016 +0100
@@ -1154,7 +1154,4 @@
 abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   where "transP r \<equiv> trans {(x, y). r x y}"  (* FIXME drop *)
 
-abbreviation (input) "RangeP \<equiv> Rangep"
-abbreviation (input) "DomainP \<equiv> Domainp"
-
 end