typo
authortraytel
Fri Sep 19 10:40:56 2014 +0200 (2014-09-19)
changeset 583866999f55645ea
parent 58385 9cbef70cff8e
child 58387 bc35a30cf0f2
typo
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Transfer.thy	Fri Sep 19 10:00:34 2014 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Fri Sep 19 10:40:56 2014 +0200
     1.3 @@ -263,7 +263,7 @@
     1.4  lemma Domainp_iff: "Domainp T x \<longleftrightarrow> (\<exists>y. T x y)"
     1.5    by auto
     1.6  
     1.7 -lemma Domaimp_refl[transfer_domain_rule]:
     1.8 +lemma Domainp_refl[transfer_domain_rule]:
     1.9    "Domainp T = Domainp T" ..
    1.10  
    1.11  lemma Domainp_prod_fun_eq[relator_domain]: