# HG changeset patch
# User nipkow
# Date 1097593196 -7200
# Node ID 1a4b471b1afa35f6dcac18b2bc0baf65bedd0884
# Parent  a3949068537edc1732424aed74045c789e235974
*** empty log message ***

diff -r a3949068537e -r 1a4b471b1afa NEWS
--- a/NEWS	Tue Oct 12 11:48:21 2004 +0200
+++ b/NEWS	Tue Oct 12 16:59:56 2004 +0200
@@ -151,6 +151,11 @@
  
 *** HOL ***
 
+* Datatype induction via method `induct' now preserves the name of the
+  induction variable. For example, when proving P(xs::'a list) by induction
+  on xs, the induction step is now P(xs) ==> P(a#xs) rather than
+  P(list) ==> P(a#list) as previously.
+
 * HOL/record: reimplementation of records. Improved scalability for
   records with many fields, avoiding performance problems for type
   inference. Records are no longer composed of nested field types, but