fixed \<0>..\<9> (-> \<zero>..\<nine>)

--- a/NEWS	Mon May 05 13:42:16 2003 +0200
+++ b/NEWS	Mon May 05 13:52:19 2003 +0200
@@ -191,7 +191,8 @@
 * \<euro> now needs package babel/greek instead of marvosym (which
 broke \Rightarrow)
 
-* normal size for \<0>...\<9> (uses \mathbf instead of textcomp package)
+* normal size for \<zero>...\<nine> (uses \mathbf instead of 
+textcomp package)
 
 
 New in Isabelle2002 (March 2002)