NEWS
changeset 22316 f662831459de
parent 22218 30a8890d2967
child 22376 b711c2ad7507
     1.1 --- a/NEWS	Tue Feb 13 18:26:48 2007 +0100
     1.2 +++ b/NEWS	Wed Feb 14 10:06:12 2007 +0100
     1.3 @@ -79,8 +79,6 @@
     1.4  
     1.5  Reasonable default setup of framework in HOL/Main.
     1.6  
     1.7 -See HOL/ex/Code*.thy for examples.
     1.8 -
     1.9  Theorem attributs for selecting and transforming function equations theorems:
    1.10  
    1.11      [code fun]:       select a theorem as function equation for a specific constant
    1.12 @@ -507,6 +505,10 @@
    1.13  
    1.14  *** HOL ***
    1.15  
    1.16 +* Addes class (axclass + locale) "preorder" as superclass of "order";
    1.17 +potential INCOMPATIBILITY: order of proof goals in order/linorder instance
    1.18 +proofs changed.
    1.19 +
    1.20  * Dropped lemma duplicate def_imp_eq in favor of meta_eq_to_obj_eq.
    1.21  INCOMPATIBILITY.
    1.22  
    1.23 @@ -517,8 +519,7 @@
    1.24  type "'a::size ==> bool"
    1.25  
    1.26  * Renamed constants "Divides.op div", "Divides.op mod" and "Divides.op
    1.27 -dvd" to "Divides.div", "Divides.mod" and "Divides.dvd"
    1.28 -"Divides.dvd". INCOMPATIBILITY.
    1.29 +dvd" to "Divides.div", "Divides.mod" and "Divides.dvd". INCOMPATIBILITY.
    1.30  
    1.31  * Added method "lexicographic_order" automatically synthesizes
    1.32  termination relations as lexicographic combinations of size measures