diff -r e8990d0e3965 -r 73939a9b70a3 NEWS --- a/NEWS Tue Aug 02 11:49:30 2016 +0200 +++ b/NEWS Tue Aug 02 17:35:18 2016 +0200 @@ -111,6 +111,12 @@ * Completion templates for commands involving "begin ... end" blocks, e.g. 'context', 'notepad'. +* Additional abbreviations for syntactic completion may be specified in +within the theory header as 'abbrevs', in addition to global +$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs. The +theory syntax for 'keywords' has been simplified accordingly: optional +abbrevs need to go into the new 'abbrevs' section. + *** Isar ***