* Isar/HOL: method 'induct' now handles non-atomic goals; as a
consequence, it is no longer monotonic wrt. the local goal context
(which is now passed through the inductive cases);

--- a/NEWS	Mon Nov 06 22:47:41 2000 +0100
+++ b/NEWS	Mon Nov 06 22:48:42 2000 +0100
@@ -10,6 +10,10 @@
 
 * Isar: 'obtain' no longer declares "that" fact as simp/intro;
 
+* Isar/HOL: method 'induct' now handles non-atomic goals; as a
+consequence, it is no longer monotonic wrt. the local goal context
+(which is now passed through the inductive cases);
+
 
 *** Document preparation ***
 
@@ -42,6 +46,9 @@
 * Pure: ?thesis / ?this / "..." now work for pure meta-level
 statements as well;
 
+* HOL: improved method 'induct' --- now handles non-atomic goals
+(potential INCOMPATIBILITY); tuned error handling;
+
 
 *** HOL ***