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