# HG changeset patch
# User krauss
# Date 1197886303 -3600
# Node ID 156660ab8a39c8063191acd3541e6e701fe9b7c0
# Parent  3316156a5a24dbbed1391a7f987a27afa80a979c
spread NEWS about "induction_scheme" method

diff -r 3316156a5a24 -r 156660ab8a39 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 ***