| changeset 53012 | cb82606b8215 |
| parent 52146 | ceb31e1ded30 |
| child 53017 | 0f376701e83b |
--- a/src/HOL/Rat.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/Rat.thy Tue Aug 13 15:59:22 2013 +0200 @@ -49,8 +49,8 @@ morphisms Rep_Rat Abs_Rat by (rule part_equivp_ratrel) -lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp cr_rat = (\<lambda>x. snd x \<noteq> 0)" -by (simp add: rat.domain) +lemma Domainp_cr_rat [transfer_domain_rule]: "Domainp pcr_rat = (\<lambda>x. snd x \<noteq> 0)" +by (simp add: rat.domain_eq) subsubsection {* Representation and basic operations *}