NEWS
changeset 15242 1a4b471b1afa
parent 15206 09d78ec709c7
child 15277 eb649b6dbf15
     1.1 --- a/NEWS	Tue Oct 12 11:48:21 2004 +0200
     1.2 +++ b/NEWS	Tue Oct 12 16:59:56 2004 +0200
     1.3 @@ -151,6 +151,11 @@
     1.4   
     1.5  *** HOL ***
     1.6  
     1.7 +* Datatype induction via method `induct' now preserves the name of the
     1.8 +  induction variable. For example, when proving P(xs::'a list) by induction
     1.9 +  on xs, the induction step is now P(xs) ==> P(a#xs) rather than
    1.10 +  P(list) ==> P(a#list) as previously.
    1.11 +
    1.12  * HOL/record: reimplementation of records. Improved scalability for
    1.13    records with many fields, avoiding performance problems for type
    1.14    inference. Records are no longer composed of nested field types, but