src/HOL/Relation.thy
changeset 64632 9df24b8b6c0a
parent 64584 142ac30b68fe
child 64633 5ebcf6c525f1
equal deleted inserted replaced
64631:7705926ee595 64632:9df24b8b6c0a
  1152 text \<open>Misc\<close>
  1152 text \<open>Misc\<close>
  1153 
  1153 
  1154 abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
  1154 abbreviation (input) transP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
  1155   where "transP r \<equiv> trans {(x, y). r x y}"  (* FIXME drop *)
  1155   where "transP r \<equiv> trans {(x, y). r x y}"  (* FIXME drop *)
  1156 
  1156 
  1157 abbreviation (input) "RangeP \<equiv> Rangep"
       
  1158 abbreviation (input) "DomainP \<equiv> Domainp"
       
  1159 
       
  1160 end
  1157 end