src/HOL/RealDef.thy
changeset 40815 6e2d17cc0d1d
parent 38857 97775f3e8722
child 40816 19c492929756
     1.1 --- a/src/HOL/RealDef.thy	Mon Nov 29 12:15:14 2010 +0100
     1.2 +++ b/src/HOL/RealDef.thy	Mon Nov 29 13:44:54 2010 +0100
     1.3 @@ -324,7 +324,7 @@
     1.4  
     1.5  lemma equiv_realrel: "equiv {X. cauchy X} realrel"
     1.6    using refl_realrel sym_realrel trans_realrel
     1.7 -  by (rule equiv.intro)
     1.8 +  by (rule equivI)
     1.9  
    1.10  subsection {* The field of real numbers *}
    1.11