1.1 --- a/doc-src/extra.sty	Mon Aug 28 10:16:58 2000 +0200
     1.2 +++ b/doc-src/extra.sty	Mon Aug 28 13:48:14 2000 +0200
     1.3 @@ -2,10 +2,6 @@
     1.4  %
     1.5  \typeout{Document Style extra. Released 17/2/94, version of 22/8/00}
     1.6  
     1.7 -\usepackage{ttbox}
     1.8 -{\obeylines\gdef\ttbreak
     1.9 -{\allowbreak}}
    1.10 -
    1.11  %%Euro-style date: 20 September 1955
    1.12  \def\today{\number\day\space\ifcase\month\or
    1.13  January\or February\or March\or April\or May\or June\or