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 ...".