--- a/NEWS Mon Jan 13 14:11:02 2014 +0100
+++ b/NEWS Mon Jan 13 18:47:48 2014 +0100
@@ -34,9 +34,10 @@
*** Pure ***
* More thorough check of proof context for goal statements and
-attributed fact expressions: background theory, declared hyps,
-declared variable names. Potential INCOMPATIBILITY, tools need to
-observe standard context discipline.
+attributed fact expressions (concerning background theory, declared
+hyps). Potential INCOMPATIBILITY, tools need to observe standard
+context discipline. See also Assumption.add_assumes and the more
+primitive Thm.assume_hyps.
*** HOL ***