tuned;
authorwenzelm
Fri Oct 06 16:11:53 2000 +0200 (2000-10-06)
changeset 10162947b7b8b0a69
parent 10161 4a3cd038aff8
child 10163 d1972b445ece
tuned;
ANNOUNCE
Admin/page/dist-content/docs.content
Admin/page/dist-content/packages.content
Admin/page/main-content/index.content
     1.1 --- a/ANNOUNCE	Fri Oct 06 15:15:19 2000 +0200
     1.2 +++ b/ANNOUNCE	Fri Oct 06 16:11:53 2000 +0200
     1.3 @@ -30,6 +30,10 @@
     1.4      virtual machine and a specification of its bytecode verifier and a
     1.5      lightweight bytecode verifier, including proofs of type-safety.
     1.6  
     1.7 +  * HOL/BCV (Tobias Nipkow)
     1.8 +    Generic model of bytecode verification, i.e. data-flow
     1.9 +    analysis for assembly languages with subtypes.
    1.10 +
    1.11    * HOL/Real (Jacques Fleuriot)
    1.12      More on nonstandard real analysis.
    1.13  
     2.1 --- a/Admin/page/dist-content/docs.content	Fri Oct 06 15:15:19 2000 +0200
     2.2 +++ b/Admin/page/dist-content/docs.content	Fri Oct 06 16:11:53 2000 +0200
     2.3 @@ -4,15 +4,25 @@
     2.4  %body%
     2.5  <!-- _GP_ distname --> documentation is included here as browsable PDF
     2.6  for convenience.  These documents are also part of the standard
     2.7 -Isabelle distribution.
     2.8 +Isabelle distribution.  For getting started with Isabelle quickly, we
     2.9 +recommend the <a href="tutorial.pdf">Tutorial on Isabelle/HOL</a>.
    2.10  
    2.11  <!-- _GP_ include("$pwd/docu-contents.dist") -->
    2.12  
    2.13 -The following text files of the Isabelle distribution may be also of
    2.14 -some interest:
    2.15 +The Isabelle distribution also includes a few text files with further
    2.16 +information about the present release and additional installation
    2.17 +instructions.
    2.18  <ul>
    2.19  <li> <!-- _GP_ href(distname . "/ANNOUNCE", "ANNOUNCE") -->
    2.20  <li> <!-- _GP_ href(distname . "/README.html", "README") -->
    2.21  <li> <!-- _GP_ href(distname . "/INSTALL", "INSTALL") -->
    2.22  <li> <!-- _GP_ href(distname . "/NEWS", "NEWS") -->
    2.23  </ul>
    2.24 +
    2.25 +<p>
    2.26 +
    2.27 +Use the mailing list <a href="mailto:
    2.28 +isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> and its
    2.29 +<a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to discuss
    2.30 +problems and results.  Why not <a
    2.31 +href="mailto:lcp@cl.cam.ac.uk">subscribe</a>?
     3.1 --- a/Admin/page/dist-content/packages.content	Fri Oct 06 15:15:19 2000 +0200
     3.2 +++ b/Admin/page/dist-content/packages.content	Fri Oct 06 16:11:53 2000 +0200
     3.3 @@ -118,6 +118,8 @@
     3.4  
     3.5  <p>
     3.6  
     3.7 -Users can now invoke the Isabelle executables without further ado.
     3.8 +Users can now invoke the Isabelle executables without further ado,
     3.9 +e.g. just start the main <tt>Isabelle</tt> executable to lauch the
    3.10 +Isabelle Proof General interface.
    3.11  
    3.12  <p>
     4.1 --- a/Admin/page/main-content/index.content	Fri Oct 06 15:15:19 2000 +0200
     4.2 +++ b/Admin/page/main-content/index.content	Fri Oct 06 16:11:53 2000 +0200
     4.3 @@ -55,6 +55,6 @@
     4.4  Use the mailing list <a href="mailto:
     4.5  isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> 
     4.6  and its <a href="ftp://ftp.cl.cam.ac.uk/ml/index.html">archive</a> to
     4.7 -discuss problems and results.  Why not <A
     4.8 -HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>? 
     4.9 +discuss problems and results.  Why not <a
    4.10 +href="mailto:lcp@cl.cam.ac.uk">subscribe</a>? 
    4.11