--- 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.
--- 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>?
--- 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>
--- 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>?