# HG changeset patch
# User wenzelm
# Date 903985799 -7200
# Node ID 57165d7271b5c16c655e63018200fb78d00c9ecc
# Parent  610abcc48c5df83c9ed8dfdc897a06e614033980
tuned;

diff -r 610abcc48c5d -r 57165d7271b5 NEWS
--- a/NEWS	Mon Aug 24 19:13:00 1998 +0200
+++ b/NEWS	Mon Aug 24 21:09:59 1998 +0200
@@ -9,6 +9,8 @@
 
 * several changes of proof tools;
 
+* HOL: new version of inductive and datatype;
+
 * HOL: major changes to the inductive and datatype packages;
 
 * HOL: renamed r^-1 to 'converse' from 'inverse'; `inj_onto' is now
@@ -262,13 +264,15 @@
 
 * improved the theory data mechanism to support encapsulation (data
 kind name replaced by private Object.kind, acting as authorization
-key); new type-safe user interface via functor TheoryDataFun;
+key); new type-safe user interface via functor TheoryDataFun; generic
+print_data function becomes basically useless;
 
 * removed global_names compatibility flag -- all theory declarations
 are qualified by default;
 
 * module Pure/Syntax now offers quote / antiquote translation
 functions (useful for Hoare logic etc. with implicit dependencies);
+see HOL/ex/Antiquote for an example use;
 
 * Simplifier now offers conversions (asm_)(full_)rewrite: simpset ->
 cterm -> thm;