| changeset 60229 | 4cd6462c1fda |
| parent 59523 | 860fb1c65553 |
| child 60758 | d8d85a8172b5 |
--- a/src/HOL/Transfer.thy Fri Dec 05 14:14:36 2014 +0100 +++ b/src/HOL/Transfer.thy Fri Dec 05 14:14:36 2014 +0100 @@ -269,6 +269,8 @@ lemma Domainp_refl[transfer_domain_rule]: "Domainp T = Domainp T" .. +lemma Domain_eq_top: "Domainp op= = top" by auto + lemma Domainp_prod_fun_eq[relator_domain]: "Domainp (op= ===> T) = (\<lambda>f. \<forall>x. (Domainp T) (f x))" by (auto intro: choice simp: Domainp_iff rel_fun_def fun_eq_iff)