1.1 --- a/NEWS	Mon Aug 24 19:13:00 1998 +0200
     1.2 +++ b/NEWS	Mon Aug 24 21:09:59 1998 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  
     1.5  * several changes of proof tools;
     1.6  
     1.7 +* HOL: new version of inductive and datatype;
     1.8 +
     1.9  * HOL: major changes to the inductive and datatype packages;
    1.10  
    1.11  * HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now
    1.12 @@ -262,13 +264,15 @@
    1.13  
    1.14  * improved the theory data mechanism to support encapsulation (data
    1.15  kind name replaced by private Object.kind, acting as authorization
    1.16 -key); new type-safe user interface via functor TheoryDataFun;
    1.17 +key); new type-safe user interface via functor TheoryDataFun; generic
    1.18 +print_data function becomes basically useless;
    1.19  
    1.20  * removed global_names compatibility flag -- all theory declarations
    1.21  are qualified by default;
    1.22  
    1.23  * module Pure/Syntax now offers quote / antiquote translation
    1.24  functions (useful for Hoare logic etc. with implicit dependencies);
    1.25 +see HOL/ex/Antiquote for an example use;
    1.26  
    1.27  * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
    1.28  cterm -> thm;