NEWS
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.