NEWS
changeset 11043 2e3bbac8763b
parent 11016 8f8ba41a5e7a
child 11050 ac5709ac50b9
     1.1 --- a/NEWS	Sat Feb 03 12:41:38 2001 +0100
     1.2 +++ b/NEWS	Sat Feb 03 15:20:55 2001 +0100
     1.3 @@ -4,6 +4,11 @@
     1.4  
     1.5  *** Overview of INCOMPATIBILITIES ***
     1.6  
     1.7 +* HOL: inductive package no longer splits induction rule aggressively,
     1.8 +but only as far as specified by the introductions given; the old
     1.9 +format may recovered via ML function complete_split_rule or attribute
    1.10 +'split_rule (complete)';
    1.11 +
    1.12  * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,
    1.13  gfp_Tarski to gfp_unfold;
    1.14