changeset 59739 | 4ed50ebf5d36 |
parent 59731 | 7fccaeec22f0 |
child 59746 | ddae5727c5a9 |
--- a/NEWS Tue Mar 17 17:45:03 2015 +0000 +++ b/NEWS Wed Mar 18 13:51:33 2015 +0100 @@ -76,6 +76,9 @@ *** HOL *** +* New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for + single-step rewriting with subterm selection based on patterns. + * the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}" type, so in particular on "real" and "complex" uniformly. Minor INCOMPATIBILITY: type constraints may be needed.