# HG changeset patch
# User wenzelm
# Date 1201555647 -3600
# Node ID c973b498127697922a8b22b431141aaef0ef6155
# Parent  431ab3907291487bf79f1809a8551578335beada
* Outer syntax: string tokens no longer admit escaped white space;

diff -r 431ab3907291 -r c973b4981276 NEWS
--- a/NEWS	Mon Jan 28 22:27:26 2008 +0100
+++ b/NEWS	Mon Jan 28 22:27:27 2008 +0100
@@ -13,6 +13,10 @@
 specified via 3 decimal digits (as in SML).  E.g. "foo\095bar" for
 "foo_bar".
 
+* Outer syntax: string tokens no longer admit escaped white space,
+which was an accidental (undocumented) feature.  INCOMPATIBILITY, use
+white space directly.
+
 * Theory loader: use_thy (and similar operations) no longer set the
 implicit ML context, which was occasionally hard to predict and in
 conflict with concurrency.  INCOMPATIBILITY, use ML within Isar which