1.1 --- a/NEWS	Fri Nov 30 17:55:13 2001 +0100
     1.2 +++ b/NEWS	Sat Dec 01 18:50:41 2001 +0100
     1.3 @@ -158,6 +158,12 @@
     1.4  
     1.5    - remove all special provisions on numerals in proofs;
     1.6  
     1.7 +* HOL: the class of all HOL types is now called "type" rather than
     1.8 +"term"; INCOMPATIBILITY, need to adapt references to this type class
     1.9 +in axclass/classes, instance/arities, and (usually rare) occurrences
    1.10 +in typings (of consts etc.); internally the class is called
    1.11 +"HOL.type", ML programs should refer to HOLogic.typeS;
    1.12 +
    1.13  * HOL/record package improvements:
    1.14    - new derived operations "fields" to build a partial record section,
    1.15      "extend" to promote a fixed record to a record scheme, and