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