author | oheimb |
Thu, 15 Feb 2001 13:07:03 +0100 | |
changeset 11130 | d14fd58615b9 |
parent 11129 | 6f6892bea902 |
child 11131 | 5dc3b5abdbca |
--- 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,