spread NEWS about "induction_scheme" method
authorkrauss
Mon, 17 Dec 2007 11:11:43 +0100
changeset 25664 156660ab8a39
parent 25663 3316156a5a24
child 25665 faabc08af882
spread NEWS about "induction_scheme" method
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 ***