# HG changeset patch
# User wenzelm
# Date 973547322 -3600
# Node ID 58bb50f694970038118fe3b0ef665b54f4ebb383
# Parent  8621cb0021a648784a8eb308742b5220116251b1
* 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);

diff -r 8621cb0021a6 -r 58bb50f69497 NEWS
--- 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 ***