# HG changeset patch
# User wenzelm
# Date 1127834667 -7200
# Node ID c98508731bd6c1fe0707661c2f556b2e087b2a30
# Parent  d7f78036546b5f3f7aac5a7172010ce020f2453d
more details about incomplete 'defs';

diff -r d7f78036546b -r c98508731bd6 ANNOUNCE
--- a/ANNOUNCE	Tue Sep 27 17:14:27 2005 +0200
+++ b/ANNOUNCE	Tue Sep 27 17:24:27 2005 +0200
@@ -5,7 +5,7 @@
 
 This release provides substantial advances over Isabelle2004, see the
 first 1000 lines of NEWS in the distribution for more details.  Some
-notable highlights are:
+notable features are:
 
 * Interpretation of locale expressions in theories, locales, and proof
 contexts.
@@ -23,6 +23,9 @@
 
 * Major internal reorganizations and performance improvements.
 
+* 'defs': more checks for overloading, but less checks for cyclic
+dependencies!
+
 
 You may get Isabelle2005 from the following mirror sites:
 
diff -r d7f78036546b -r c98508731bd6 Admin/website/index.html
--- a/Admin/website/index.html	Tue Sep 27 17:14:27 2005 +0200
+++ b/Admin/website/index.html	Tue Sep 27 17:24:27 2005 +0200
@@ -45,7 +45,7 @@
           </p>
 
         <h2>Now available: Isabelle 2005</h2>
-         <p>Some notable highlights:</p>
+         <p>Some notable features:</p>
               <ul>
 	      <li>Interpretation of locale expressions in theories, locales, and proof contexts.</li>
 	      <li>Substantial library improvements (HOL, HOL-Complex, HOLCF).</li>
@@ -54,6 +54,9 @@
 	      <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>
+              <li>More well-formedness checks of overloaded
+                  definitions, but fails to recognize certain ill-formed definitions
+                  that Isabelle2004 would have rejected outright!</li>
 	      </ul>
 
 <p><a href="//dist/Isabelle/NEWS">[Cumulative NEWS]</a></p>
diff -r d7f78036546b -r c98508731bd6 NEWS
--- a/NEWS	Tue Sep 27 17:14:27 2005 +0200
+++ b/NEWS	Tue Sep 27 17:24:27 2005 +0200
@@ -204,7 +204,9 @@
 rather than 'types'.  INCOMPATIBILITY for new object-logic
 specifications.
 
-* 'defs': more well-formedness checks of overloaded definitions.
+* 'defs': more well-formedness checks of overloaded definitions, but
+still does not cover all situations.  Even fails to recognize certain
+ill-formed definitions that Isabelle2004 would have rejected outright!
 
 * Attributes 'induct' and 'cases': type or set names may now be
 locally fixed variables as well.