# HG changeset patch
# User kleing
# Date 1082081212 -7200
# Node ID 37a92211a5d363610fea965e3b928c8f183aafba
# Parent  c721a0d251b09defcf6c700373a5993544867e13
add feature list

diff -r c721a0d251b0 -r 37a92211a5d3 Admin/page/main-content/index.content
--- a/Admin/page/main-content/index.content	Fri Apr 16 04:06:25 2004 +0200
+++ b/Admin/page/main-content/index.content	Fri Apr 16 04:06:52 2004 +0200
@@ -35,6 +35,44 @@
 
 <p>
 
+<h2><!-- _GP_ distname --></h2>
+New features in <strong><!-- _GP_ distname --></strong> include
+<ul>
+<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>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>
+
+<li>Improved locales (named proof contexts), instantiation of locales.</li>
+
+<li>Improved calculational reasoning chains.</li>
+
+<li>Improved records handling.</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>refute</code> command to search for (finite) countermodels for a fragment of HOL.</li>
+
+<li>Presentation and x-symbol enhancements, greek letters and sub/superscripts in identifiers.</li>
+</ul>
+<a href="dist/<!-- _GP_ distname -->/NEWS">[Complete Changelog]</a>
+<p>
+The <strong><!-- _GP_ distname --></strong> distribution is available
+from several <a href="dist/index.html">mirror sites</a>.  It includes
+source and binary packages and browsable documentation. There is also
+a nightly generated <a href="http://isabelle.in.tum.de/devel/">development 
+snapshot</a> available.
+
+<p>
+
 <h2>Out now</h2>
 
 The 
@@ -44,16 +82,6 @@
 
 <p>
 
-<h2>Obtaining Isabelle</h2>
-
-The <strong><!-- _GP_ distname --></strong> distribution is available
-from several <a href="dist/index.html">mirror sites</a>.  It includes
-source and binary packages and browsable documentation. There is also
-a nightly generated <a href="http://isabelle.in.tum.de/devel/">development 
-snapshot</a> available.
-
-<p>
-
 You can also browse the <a href="library/index.html">Isabelle theory
 library</a>; the main logics are <a
 href="library/HOL/index.html">HOL</a>, <a