# HG changeset patch
# User huffman
# Date 1291134904 28800
# Node ID 142f890ceef67bee0432cda98c98946ed6cb2c24
# Parent  86dff9dfd8069b84dcaf7f974dd4cb06126d1672
use new 'file' antiquotation for reference to Dedekind_Real.thy

diff -r 86dff9dfd806 -r 142f890ceef6 src/HOL/RealDef.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 *}