author | krauss |
Mon, 17 Dec 2007 11:11:43 +0100 | |
changeset 25664 | 156660ab8a39 |
parent 25663 | 3316156a5a24 |
child 25665 | faabc08af882 |
--- 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 ***