NEWS
changeset 11130 d14fd58615b9
parent 11124 5b97a468b46d
child 11169 98c2f741e32b
equal deleted inserted replaced
11129:6f6892bea902 11130:d14fd58615b9
     7 
     7 
     8 *** Overview of INCOMPATIBILITIES ***
     8 *** Overview of INCOMPATIBILITIES ***
     9 
     9 
    10 * HOL: inductive package no longer splits induction rule aggressively,
    10 * HOL: inductive package no longer splits induction rule aggressively,
    11 but only as far as specified by the introductions given; the old
    11 but only as far as specified by the introductions given; the old
    12 format may recovered via ML function complete_split_rule or attribute
    12 format may be recovered via ML function complete_split_rule or attribute
    13 'split_rule (complete)';
    13 'split_rule (complete)';
    14 
    14 
    15 * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,
    15 * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,
    16 gfp_Tarski to gfp_unfold;
    16 gfp_Tarski to gfp_unfold;
    17 
    17