# HG changeset patch
# User wenzelm
# Date 1389635268 -3600
# Node ID ea9fc64327cbc88a251641185925559deb18904f
# Parent  38ea5ee18a060016a9a5962091fa46e9f2646d3a
tuned;

diff -r 38ea5ee18a06 -r ea9fc64327cb NEWS
--- 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 ***