src/HOL/Rat.thy
changeset 45694 4a8743618257
parent 45507 6975db7fd6f0
child 45818 53a697f5454a
     1.1 --- a/src/HOL/Rat.thy	Wed Nov 30 16:05:15 2011 +0100
     1.2 +++ b/src/HOL/Rat.thy	Wed Nov 30 16:27:10 2011 +0100
     1.3 @@ -54,7 +54,11 @@
     1.4    shows "ratrel `` {x} = ratrel `` {y} \<longleftrightarrow> (x, y) \<in> ratrel"
     1.5    by (rule eq_equiv_class_iff, rule equiv_ratrel) (auto simp add: assms)
     1.6  
     1.7 -typedef (Rat) rat = "{x. snd x \<noteq> 0} // ratrel"
     1.8 +definition "Rat = {x. snd x \<noteq> 0} // ratrel"
     1.9 +
    1.10 +typedef (open) rat = Rat
    1.11 +  morphisms Rep_Rat Abs_Rat
    1.12 +  unfolding Rat_def
    1.13  proof
    1.14    have "(0::int, 1::int) \<in> {x. snd x \<noteq> 0}" by simp
    1.15    then show "ratrel `` {(0, 1)} \<in> {x. snd x \<noteq> 0} // ratrel" by (rule quotientI)