1.1 --- a/doc-src/ERRATA.txt	Tue Feb 10 12:02:11 2004 +0100
     1.2 +++ b/doc-src/ERRATA.txt	Tue Feb 10 12:17:04 2004 +0100
     1.3 @@ -122,9 +122,9 @@
     1.4  first.
     1.5  
     1.6  page 259: HOL theory files may now include datatype declarations, primitive
     1.7 -recursive function definitions, and (co)inductive definitions.  (These new
     1.8 -sections are available separately as the file ml/HOL-extensions.dvi.gz,
     1.9 -host ftp.cl.cam.ac.uk.)
    1.10 +recursive function definitions, and (co)inductive definitions.  These new
    1.11 +sections are available separately at
    1.12 +    http://www.cl.cam.ac.uk/users/lcp/archive/ml/HOL-extensions.dvi.gz
    1.13  
    1.14  page 259: now there is another examples directory, IMP (a semantics
    1.15  equivalence proof for an imperative language)