| changeset 11043 | 2e3bbac8763b |
| parent 11016 | 8f8ba41a5e7a |
| child 11050 | ac5709ac50b9 |
--- a/NEWS Sat Feb 03 12:41:38 2001 +0100 +++ b/NEWS Sat Feb 03 15:20:55 2001 +0100 @@ -4,6 +4,11 @@ *** Overview of INCOMPATIBILITIES *** +* 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 +'split_rule (complete)'; + * HOL: induct renamed to lfp_induct, lfp_Tarski to lfp_unfold, gfp_Tarski to gfp_unfold;