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