fixed \<0>..\<9> (-> \<zero>..\<nine>)
authorkleing
Mon May 05 13:52:19 2003 +0200 (2003-05-05)
changeset 139542e989faba65a
parent 13953 65b76920e108
child 13955 8ab1d3e73bb1
fixed \<0>..\<9> (-> \<zero>..\<nine>)
NEWS
     1.1 --- a/NEWS	Mon May 05 13:42:16 2003 +0200
     1.2 +++ b/NEWS	Mon May 05 13:52:19 2003 +0200
     1.3 @@ -191,7 +191,8 @@
     1.4  * \<euro> now needs package babel/greek instead of marvosym (which
     1.5  broke \Rightarrow)
     1.6  
     1.7 -* normal size for \<0>...\<9> (uses \mathbf instead of textcomp package)
     1.8 +* normal size for \<zero>...\<nine> (uses \mathbf instead of 
     1.9 +textcomp package)
    1.10  
    1.11  
    1.12  New in Isabelle2002 (March 2002)