use new 'file' antiquotation for reference to Dedekind_Real.thy

--- 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 *}