# HG changeset patch
# User wenzelm
# Date 979601861 -3600
# Node ID 6b66a8a530ce6f63d9b48f2b3ef20aeb4523c5b2
# Parent  aded4ba99b88319d6fdb5d8baef55be5057b5a82
* 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);

diff -r aded4ba99b88 -r 6b66a8a530ce NEWS
--- 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;