# HG changeset patch
# User kleing
# Date 1082724432 -7200
# Node ID a68de9a2770a0f66db00daa9740e7180e9218b60
# Parent  b1293d0f8d5fedb70f1adc27034e9d72d6c6b5e9
add link to HOL4 libraries

diff -r b1293d0f8d5f -r a68de9a2770a Admin/page/main-content/logics.content
--- a/Admin/page/main-content/logics.content	Fri Apr 23 11:04:07 2004 +0200
+++ b/Admin/page/main-content/logics.content	Fri Apr 23 14:47:12 2004 +0200
@@ -21,8 +21,10 @@
 <dt><a
 href="library/HOL/index.html"><strong>Isabelle/HOL</strong></a><dd> is
 a version of classical higher-order logic resembling that of the <A
-HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL
-System</A>.
+HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</A>. The
+main libraries of the HOL 4 System are now <a
+href="library/HOL/HOL-Complex/HOL4/index.html">available in
+Isabelle</a>.
 
 <dt><a
 href="library/HOLCF/index.html"><strong>Isabelle/HOLCF</strong></a><dd>