NEWS

--- a/NEWS	Sun Dec 16 22:37:55 2007 +0100
+++ b/NEWS	Mon Dec 17 11:11:43 2007 +0100
@@ -43,6 +43,12 @@
 Sup_set_def, le_def, less_def, option_map_def now with object
 equality.
 
+* New method "induction_scheme" derives user-specified induction rules
+from wellfounded induction and completeness of patterns. This factors
+out some operations that are done internally by the function package
+and makes them available separately. See "HOL/ex/Induction_Scheme.thy"
+for examples,
+
 
 *** System ***