NEWS
changeset 28685 275122631271
parent 28676 78688a5fafc2
child 28700 fb92b1d1b285
     1.1 --- a/NEWS	Fri Oct 24 17:48:36 2008 +0200
     1.2 +++ b/NEWS	Fri Oct 24 17:48:37 2008 +0200
     1.3 @@ -104,10 +104,19 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New classes "top" and "bot" with corresponding operations "top" and "bot"
     1.8 +in theory Orderings;  instantiation of class "complete_lattice" requires
     1.9 +instantiation of classes "top" and "bot".  INCOMPATIBILITY.
    1.10 +
    1.11 +* Changed definition lemma "less_fun_def" in order to provide an instance
    1.12 +for preorders on functions;  use lemma "less_le" instead.  INCOMPATIBILITY.
    1.13 +
    1.14  * Unified theorem tables for both code code generators.  Thus
    1.15  [code func] has disappeared and only [code] remains.  INCOMPATIBILITY.
    1.16  
    1.17 -* Constant "undefined" replaces "arbitrary" in most occurences.
    1.18 +* Constants "undefined" and "default" replace "arbitrary".  Usually
    1.19 +"undefined" is the right choice to replace "arbitrary", though logically
    1.20 +there is no difference.  INCOMPATIBILITY.
    1.21  
    1.22  * Generic ATP manager for Sledgehammer, based on ML threads instead of
    1.23  Posix processes.  Avoids potentially expensive forking of the ML