# HG changeset patch
# User paulson
# Date 1052755904 -7200
# Node ID 5fc9474833e563a6ec5e70905923a5c9e331c4a9
# Parent  b141b26145e107ceb5a3d74fb28d07e431c972d5
oops

diff -r b141b26145e1 -r 5fc9474833e5 src/HOL/Complex/README.html
--- a/src/HOL/Complex/README.html	Mon May 12 15:57:46 2003 +0200
+++ b/src/HOL/Complex/README.html	Mon May 12 18:11:44 2003 +0200
@@ -5,7 +5,7 @@
 <P>This directory defines the type <KBD>complex</KBD> of the complex numbers,
 with numeric constants and some complex analysis.  The development includes
 nonstandard analysis for the complex numbers.  Note that the image
-<KBD>Complex</KBD> includes theories from the directories 
+<KBD>HOL-Complex</KBD> includes theories from the directories 
 <KBD>HOL/Real</KBD>  and <KBD>HOL/Hyperreal</KBD>.
 
 <HR>