--- a/NEWS Fri Aug 12 14:02:48 2016 +0200
+++ b/NEWS Fri Aug 12 14:19:27 2016 +0200
@@ -136,17 +136,15 @@
before. The theory syntax for 'keywords' has been simplified
accordingly: optional abbrevs need to go into the new 'abbrevs' section.
-
-*** Document preparation ***
-
-* Document antiquotations for file-systems paths are more specific and
-diverse:
-
- @{path NAME} -- no check (formerly @{file_unchecked})
- @{file NAME} -- plain file (formerly file or directory)
- @{dir NAME} -- directory (formerly subsumed by @{file})
-
-Minor INCOMPATIBILITY.
+* ML and document antiquotations for file-systems paths are more uniform
+and diverse:
+
+ @{path NAME} -- no file-system check
+ @{file NAME} -- check for plain file
+ @{dir NAME} -- check for directory
+
+Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may
+have to be changed.
*** Isar ***