diff -r 6f6892bea902 -r d14fd58615b9 NEWS --- a/NEWS Thu Feb 15 11:15:39 2001 +0100 +++ b/NEWS Thu Feb 15 13:07:03 2001 +0100 @@ -9,7 +9,7 @@ * 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 +format may be recovered via ML function complete_split_rule or attribute 'split_rule (complete)'; * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold,