use new 'file' antiquotation for reference to Dedekind_Real.thy
authorhuffman
Tue Nov 30 08:35:04 2010 -0800 (2010-11-30)
changeset 40810142f890ceef6
parent 40809 86dff9dfd806
child 40811 ab0a8cc7976a
use new 'file' antiquotation for reference to Dedekind_Real.thy
src/HOL/RealDef.thy
     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 *}