Admin/website/index.html

--- a/Admin/website/index.html	Mon Sep 26 20:51:57 2005 +0200
+++ b/Admin/website/index.html	Mon Sep 26 20:52:36 2005 +0200
@@ -44,67 +44,28 @@
           bibliography, and Isabelle workshops and courses.
           </p>
 
-        <h2>Coming soon: Isabelle 2005</h2>
-         <p>New features in the upcoming Isabelle 2005 will include</p>
+        <h2>Now available: Isabelle 2005</h2>
+         <p>Some notable highlights:</p>
               <ul>
-                <li>New commands for instantiating locales</li>
-                <li>New command for finding theorems (by term patterns, as intro/elim/simp rules, etc.)</li>
-                <li>New automatic transitivity reasoner</li>
-                <li>New command for ad-hoc theory viewing and printing</li>
-                <li>Much extended and improved theory of finite sets</li>
-                <li>New syntax that will allow &gt; and &gt;= in addition to &lt; and
-                &lt;=</li>
-              </ul>
-
-        <h2>Isabelle 2004</h2> 
-
-<p>New features in Isabelle 2004 include</p>
-
-<ul>
-<li>New image HOL4 with imported library from HOL4 system on top of
-  HOL-Complex (about 2500 additional theorems).</li>
-
-<li>New theory Ring_and_Field with over 250 basic numerical laws, 
-  all proved in axiomatic type classes for semirings, rings and fields.</li>
-
-<li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li>
+	      <li>Interpretation of locale expressions in theories, locales, and proof contexts.</li>
+	      <li>Substantial library improvements (HOL, HOL-Complex, HOLCF).</li>
+	      <li>Proof tools for transitivity reasoning.</li>
+	      <li>General <code>find_theorems</code> command (by term patterns, as intro/elim/simp rules etc.).</li>
+	      <li>Commands for generating adhoc draft documents.</li>
+	      <li>Support for Unicode proof documents (UTF-8).</li>
+	      <li>Major internal reorganizations and performance improvements.</li>
+	      </ul>
 
-<li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>
-
-<li>New theory of matrices with an application to linear programming in HOL-Matrix.</li>
-
-<li>Improved locales (named proof contexts), instantiation of locales.</li>
-
-<li>Improved handling of linear and partial orders in simplifier.</li>
- 
-<li>New <code>specification</code> command for definition by specification.</li>  
-
-<li>New Isar command <code>finalconsts</code> prevents constants being given a definition later.</li>  
-
-<li><code>arith</code> now generates counterexamples for reals as well.</li>
-
-<li>New <code>quickcheck</code> command
-    to search for counterexamples of executable goals.
-  (see HOL/ex/Quickcheck_Examples.thy)</li>
-<li>New <code>refute</code> command
-    to search for finite countermodels of goals.
-  (see HOL/ex/Refute_Examples.thy)
-</li>
-
-<li>Presentation and x-symbol enhancements, greek letters and
-sub/superscripts allowed in identifiers.</li>
-</ul>
-
-<p><a href="//dist/packages/Isabelle/NEWS">[Complete Changelog]</a></p>
+<p><a href="//dist/packages/Isabelle/NEWS">[Cumulative NEWS]</a></p>
 
 <h2>Download</h2>
 
 <p>
-The Isabelle distribution is distributed for free under the BSD license.
-It includes source and binary packages and browsable documentation,
-see the <a href="installation.html">installation instructions</a>. You can also
-browse the <a href="//dist/library/index.html">Isabelle theory library</a>
-online. 
+Isabelle is distributed for free under the BSD license.  It includes
+source and binary packages and browsable documentation, see the <a
+href="installation.html">installation instructions</a>. You can also
+browse the <a href="//dist/library/index.html">Isabelle theory
+library</a> online.
 </p>
 
 <p>