isatools "symbolinput" and "nonascii" have disappeared;

--- 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);