HOL: inductive package no longer splits induction rule aggressively,
authorwenzelm
Sat Feb 03 15:20:55 2001 +0100 (2001-02-03)
changeset 110432e3bbac8763b
parent 11042 bb566dd3f927
child 11044 5873a05b4d21
HOL: inductive package no longer splits induction rule aggressively,
but only as far as specified by the introductions given; the old
format may recovered via ML function complete_split_rule or attribute
'split_rule (complete)';
NEWS
     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