--- a/NEWS Tue Jan 16 00:35:50 2001 +0100
+++ b/NEWS Tue Jan 16 00:37:41 2001 +0100
@@ -106,6 +106,16 @@
* HOL/typedef: simplified package, provide more useful rules (see also
HOL/subset.thy);
+* HOL/datatype: induction rule for arbitrarily branching datatypes is
+now expressed as a proper nested rule (old-style tactic scripts may
+require atomize_strip_tac to cope with non-atomic premises);
+
+* HOL: renamed theory "Prod" to "Product_Type", renamed "split" rule
+to "split_conv" (old name still available for compatibility);
+
+* HOL: improved concrete syntax for strings (e.g. allows translation
+rules with string literals);
+
* HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and
Fleuriot's mechanization of analysis;