src/HOL/Rational.thy
changeset 30198 922f944f03b2
parent 30097 57df8626c23b
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Rational.thy	Mon Mar 02 08:26:03 2009 +0100
     1.2 +++ b/src/HOL/Rational.thy	Mon Mar 02 16:53:55 2009 +0100
     1.3 @@ -21,8 +21,8 @@
     1.4    "(x, y) \<in> ratrel \<longleftrightarrow> snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x"
     1.5    by (simp add: ratrel_def)
     1.6  
     1.7 -lemma refl_ratrel: "refl {x. snd x \<noteq> 0} ratrel"
     1.8 -  by (auto simp add: refl_def ratrel_def)
     1.9 +lemma refl_on_ratrel: "refl_on {x. snd x \<noteq> 0} ratrel"
    1.10 +  by (auto simp add: refl_on_def ratrel_def)
    1.11  
    1.12  lemma sym_ratrel: "sym ratrel"
    1.13    by (simp add: ratrel_def sym_def)
    1.14 @@ -44,7 +44,7 @@
    1.15  qed
    1.16    
    1.17  lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
    1.18 -  by (rule equiv.intro [OF refl_ratrel sym_ratrel trans_ratrel])
    1.19 +  by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
    1.20  
    1.21  lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
    1.22  lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]