# HG changeset patch
# User wenzelm
# Date 1465404350 -7200
# Node ID 29fe61d5f748e8d603fcd657a8de940c803fe02f
# Parent  576fb8068ba6a4700ec49509c062f31663bca2b6
NEWS;

diff -r 576fb8068ba6 -r 29fe61d5f748 NEWS
--- a/NEWS	Wed Jun 08 18:45:44 2016 +0200
+++ b/NEWS	Wed Jun 08 18:45:50 2016 +0200
@@ -98,6 +98,16 @@
 * The old proof method "default" has been removed (legacy since
 Isabelle2016). INCOMPATIBILITY, use "standard" instead.
 
+* Proof methods may refer to the main facts via the dynamic fact
+"method_facts". This is particularly useful for Eisbach method
+definitions.
+
+* Eisbach provides method "use" to modify the main facts of a given
+method expression, e.g.
+
+  (use facts in simp)
+  (use facts in \<open>simp add: ...\<close>)
+
 
 *** Pure ***