src/HOL/RealDef.thy
changeset 40810 142f890ceef6
parent 38857 97775f3e8722
child 40826 a3af470a55d2
     1.1 --- a/src/HOL/RealDef.thy	Tue Nov 30 08:00:50 2010 -0800
     1.2 +++ b/src/HOL/RealDef.thy	Tue Nov 30 08:35:04 2010 -0800
     1.3 @@ -14,8 +14,8 @@
     1.4  text {*
     1.5    This theory contains a formalization of the real numbers as
     1.6    equivalence classes of Cauchy sequences of rationals.  See
     1.7 -  \url{HOL/ex/Dedekind_Real.thy} for an alternative construction
     1.8 -  using Dedekind cuts.
     1.9 +  @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
    1.10 +  construction using Dedekind cuts.
    1.11  *}
    1.12  
    1.13  subsection {* Preliminary lemmas *}