--- a/NEWS Fri Oct 02 16:56:46 2015 +0200
+++ b/NEWS Fri Oct 02 19:34:12 2015 +0200
@@ -197,6 +197,11 @@
*** HOL ***
+* Commands 'inductive' and 'inductive_set' work better when names for
+intro rules are omitted: the "cases" and "induct" rules no longer
+declare empty case_names, but no case_names at all. This allows to use
+numbered cases in proofs, without requiring method "goal_cases".
+
* The 'typedef' command has been upgraded from a partially checked
"axiomatization", to a full definitional specification that takes the
global collection of overloaded constant / type definitions into