# HG changeset patch
# User wenzelm
# Date 1008084129 -3600
# Node ID b5630a4ea5d8ee7f73c4d8eb6d5d21a18606826c
# Parent  5f41826670320545bbd2d2402b5985db2a940c0b
isatools "symbolinput" and "nonascii" have disappeared;

diff -r 5f4182667032 -r b5630a4ea5d8 NEWS
--- a/NEWS	Tue Dec 11 16:00:26 2001 +0100
+++ b/NEWS	Tue Dec 11 16:22:09 2001 +0100
@@ -299,7 +299,8 @@
 
 * system: refrain from any attempt at filtering input streams; no
 longer support ``8bit'' encoding of old isabelle font, instead proper
-iso-latin characters may now be used;
+iso-latin characters may now be used; the related isatools
+"symbolinput" and "nonascii" have disappeared as well;
 
 * system: support Poly/ML 4.1.1 (able to manage larger heaps);