diff -r 414e3550e9c0 -r 0edec65d0633 NEWS --- a/NEWS Wed Jun 08 16:46:48 2016 +0200 +++ b/NEWS Wed Jun 08 18:46:09 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 \simp add: ...\) + *** Pure ***