# HG changeset patch
# User wenzelm
# Date 981210055 -3600
# Node ID 2e3bbac8763bf848ccac481721e2b628c46c2939
# Parent  bb566dd3f927b125f239602ad5ca782796cddb69
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)';

diff -r bb566dd3f927 -r 2e3bbac8763b NEWS
--- 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;