# HG changeset patch # User wenzelm # Date 1535911853 -7200 # Node ID feb1b1b3c51fed22e00fec51297069a27178c950 # Parent 9203eb13bef717f377b4dd268c7610da4d13e706 NEWS; diff -r 9203eb13bef7 -r feb1b1b3c51f NEWS --- a/NEWS Sun Sep 02 19:48:15 2018 +0200 +++ b/NEWS Sun Sep 02 20:10:53 2018 +0200 @@ -14,6 +14,12 @@ specified in seconds; a negative value means it is disabled (default). +*** Isar *** + +* More robust treatment of structural errors: begin/end blocks take +precedence over goal/proof. + + *** HOL *** * Simplified syntax setup for big operators under image. In rare