NEWS;
authorwenzelm
Sun, 12 Jan 2014 18:40:49 +0100
changeset 55001 f26a7f06266d
parent 55000 782b8cc9233d
child 55002 81fff1c65943
NEWS;
NEWS
--- 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 ...".