# HG changeset patch
# User wenzelm
# Date 970841513 -7200
# Node ID 947b7b8b0a69b78becfd3962a13dd80efc098393
# Parent  4a3cd038aff82ae48281d8968c1d64a63a9321eb
tuned;

diff -r 4a3cd038aff8 -r 947b7b8b0a69 ANNOUNCE
--- a/ANNOUNCE	Fri Oct 06 15:15:19 2000 +0200
+++ b/ANNOUNCE	Fri Oct 06 16:11:53 2000 +0200
@@ -30,6 +30,10 @@
     virtual machine and a specification of its bytecode verifier and a
     lightweight bytecode verifier, including proofs of type-safety.
 
+  * HOL/BCV (Tobias Nipkow)
+    Generic model of bytecode verification, i.e. data-flow
+    analysis for assembly languages with subtypes.
+
   * HOL/Real (Jacques Fleuriot)
     More on nonstandard real analysis.
 
diff -r 4a3cd038aff8 -r 947b7b8b0a69 Admin/page/dist-content/docs.content
--- a/Admin/page/dist-content/docs.content	Fri Oct 06 15:15:19 2000 +0200
+++ b/Admin/page/dist-content/docs.content	Fri Oct 06 16:11:53 2000 +0200
@@ -4,15 +4,25 @@
 %body%
 <!-- _GP_ distname --> documentation is included here as browsable PDF
 for convenience.  These documents are also part of the standard
-Isabelle distribution.
+Isabelle distribution.  For getting started with Isabelle quickly, we
+recommend the <a href="tutorial.pdf">Tutorial on Isabelle/HOL</a>.
 
 <!-- _GP_ include("$pwd/docu-contents.dist") -->
 
-The following text files of the Isabelle distribution may be also of
-some interest:
+The Isabelle distribution also includes a few text files with further
+information about the present release and additional installation
+instructions.
 <ul>
 <li> <!-- _GP_ href(distname . "/ANNOUNCE", "ANNOUNCE") -->
 <li> <!-- _GP_ href(distname . "/README.html", "README") -->
 <li> <!-- _GP_ href(distname . "/INSTALL", "INSTALL") -->
 <li> <!-- _GP_ href(distname . "/NEWS", "NEWS") -->
 </ul>
+
+<p>
+
+Use the mailing list <a href="mailto:
+isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> and its
+<a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to discuss
+problems and results.  Why not <a
+href="mailto:lcp@cl.cam.ac.uk">subscribe</a>?
diff -r 4a3cd038aff8 -r 947b7b8b0a69 Admin/page/dist-content/packages.content
--- a/Admin/page/dist-content/packages.content	Fri Oct 06 15:15:19 2000 +0200
+++ b/Admin/page/dist-content/packages.content	Fri Oct 06 16:11:53 2000 +0200
@@ -118,6 +118,8 @@
 
 <p>
 
-Users can now invoke the Isabelle executables without further ado.
+Users can now invoke the Isabelle executables without further ado,
+e.g. just start the main <tt>Isabelle</tt> executable to lauch the
+Isabelle Proof General interface.
 
 <p>
diff -r 4a3cd038aff8 -r 947b7b8b0a69 Admin/page/main-content/index.content
--- a/Admin/page/main-content/index.content	Fri Oct 06 15:15:19 2000 +0200
+++ b/Admin/page/main-content/index.content	Fri Oct 06 16:11:53 2000 +0200
@@ -55,6 +55,6 @@
 Use the mailing list <a href="mailto:
 isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> 
 and its <a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to
-discuss problems and results.  Why not <A
-HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>? 
+discuss problems and results.  Why not <a
+href="mailto:lcp@cl.cam.ac.uk">subscribe</a>?