more details about incomplete 'defs';
authorwenzelm
Tue Sep 27 17:24:27 2005 +0200 (2005-09-27)
changeset 17684c98508731bd6
parent 17683 d7f78036546b
child 17685 8e5b9790805e
more details about incomplete 'defs';
ANNOUNCE
Admin/website/index.html
NEWS
     1.1 --- a/ANNOUNCE	Tue Sep 27 17:14:27 2005 +0200
     1.2 +++ b/ANNOUNCE	Tue Sep 27 17:24:27 2005 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  This release provides substantial advances over Isabelle2004, see the
     1.6  first 1000 lines of NEWS in the distribution for more details.  Some
     1.7 -notable highlights are:
     1.8 +notable features are:
     1.9  
    1.10  * Interpretation of locale expressions in theories, locales, and proof
    1.11  contexts.
    1.12 @@ -23,6 +23,9 @@
    1.13  
    1.14  * Major internal reorganizations and performance improvements.
    1.15  
    1.16 +* 'defs': more checks for overloading, but less checks for cyclic
    1.17 +dependencies!
    1.18 +
    1.19  
    1.20  You may get Isabelle2005 from the following mirror sites:
    1.21  
     2.1 --- a/Admin/website/index.html	Tue Sep 27 17:14:27 2005 +0200
     2.2 +++ b/Admin/website/index.html	Tue Sep 27 17:24:27 2005 +0200
     2.3 @@ -45,7 +45,7 @@
     2.4            </p>
     2.5  
     2.6          <h2>Now available: Isabelle 2005</h2>
     2.7 -         <p>Some notable highlights:</p>
     2.8 +         <p>Some notable features:</p>
     2.9                <ul>
    2.10  	      <li>Interpretation of locale expressions in theories, locales, and proof contexts.</li>
    2.11  	      <li>Substantial library improvements (HOL, HOL-Complex, HOLCF).</li>
    2.12 @@ -54,6 +54,9 @@
    2.13  	      <li>Commands for generating adhoc draft documents.</li>
    2.14  	      <li>Support for Unicode proof documents (UTF-8).</li>
    2.15  	      <li>Major internal reorganizations and performance improvements.</li>
    2.16 +              <li>More well-formedness checks of overloaded
    2.17 +                  definitions, but fails to recognize certain ill-formed definitions
    2.18 +                  that Isabelle2004 would have rejected outright!</li>
    2.19  	      </ul>
    2.20  
    2.21  <p><a href="//dist/Isabelle/NEWS">[Cumulative NEWS]</a></p>
     3.1 --- a/NEWS	Tue Sep 27 17:14:27 2005 +0200
     3.2 +++ b/NEWS	Tue Sep 27 17:24:27 2005 +0200
     3.3 @@ -204,7 +204,9 @@
     3.4  rather than 'types'.  INCOMPATIBILITY for new object-logic
     3.5  specifications.
     3.6  
     3.7 -* 'defs': more well-formedness checks of overloaded definitions.
     3.8 +* 'defs': more well-formedness checks of overloaded definitions, but
     3.9 +still does not cover all situations.  Even fails to recognize certain
    3.10 +ill-formed definitions that Isabelle2004 would have rejected outright!
    3.11  
    3.12  * Attributes 'induct' and 'cases': type or set names may now be
    3.13  locally fixed variables as well.