# HG changeset patch # User oheimb # Date 982238823 -3600 # Node ID d14fd58615b9e8e8d386dd2dc96d231cc8429c40 # Parent 6f6892bea90247bc9cf225ac4b4aa125e2700d68 added missiong word 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,