src/HOL/Transfer.thy
changeset 58386 6999f55645ea
parent 58182 82478e6c60cb
child 58444 ed95293f14b6
     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]: