diff -r 8c16ec5ba62b -r 3833b58a5d88 Admin/page/main-content/docs.content
--- a/Admin/page/main-content/docs.content	Mon Sep 18 14:10:31 2000 +0200
+++ b/Admin/page/main-content/docs.content	Mon Sep 18 14:35:54 2000 +0200
@@ -3,7 +3,8 @@
 
 %body%
 
-<!-- _GP_ include("$pwd/docu-contents.main") -->
+<!-- _GP_ distname --> documentation is included here as browsable PDF
+for convenience.  These documents are also part of the standard
+Isabelle <a href="dist/">distribution</a>.
 
-All this documentation is also part of the Isabelle <a
-href="dist/">distribution</a> (both as dvi and pdf).
+<!-- _GP_ include("$pwd/docu-contents.main") -->