NEWS
changeset 55001 f26a7f06266d
parent 54893 4061ec8adb1c
child 55006 ea9fc64327cb
--- a/NEWS	Sun Jan 12 18:34:00 2014 +0100
+++ b/NEWS	Sun Jan 12 18:40:49 2014 +0100
@@ -31,6 +31,14 @@
 "isabelle jedit -m MODE".
 
 
+*** 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.
+
+
 *** HOL ***
 
 * "declare [[code abort: ...]]" replaces "code_abort ...".