changeset 11130 | d14fd58615b9 |
parent 11124 | 5b97a468b46d |
child 11169 | 98c2f741e32b |
--- 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,