\setlength{\unitlength}{0.012500in}%
\begin{picture}(320,520)(40,280)
\thicklines
\put(320,380){\oval(80,40)}
\put(320,540){\oval(80,40)}
\put(140,700){\oval(80,40)}
\put(140,540){\oval(80,40)}
\put( 40,440){\framebox(80,40){}}
\put(160,440){\framebox(80,40){}}
\put(100,600){\framebox(80,40){}}
\put(200,760){\framebox(80,40){}}
\put(280,440){\framebox(80,40){}}
\put(280,280){\framebox(80,40){}}
\put(140,680){\vector( 0,-1){ 40}}
\put(140,600){\vector( 0,-1){ 40}}
\put(320,520){\vector( 0,-1){ 40}}
\put(320,440){\vector( 0,-1){ 40}}
\put(320,360){\vector( 0,-1){ 40}}
\put(240,760){\vector(-2,-1){ 80}}
\put(240,760){\line( 2,-1){ 80}}
\put(320,720){\vector( 0,-1){160}}
\put(140,520){\vector(-3,-2){ 60}}
\put(140,520){\vector( 3,-2){ 60}}
\put(200,440){\line( 0,-1){ 30}}
\put(200,410){\line( 1, 0){ 55}}
\put(255,410){\line( 0, 1){130}}
\put(255,540){\vector( 1, 0){ 25}}
\put(140,615){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{ML file}}}
\put(240,775){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{MASTER}}}
\put(140,695){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\tangle}}}
\put(140,535){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{HOL}}}
\put( 80,455){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{THEORY}}}
\put(200,455){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{TAG FILE}}}
\put(320,455){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\LaTeX\ file}}}
\put(320,535){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\weave}}}
\put(320,375){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{\LaTeX}}}
\put(320,295){\makebox(0,0)[b]{\raisebox{0pt}[0pt][0pt]{DOCUMENT}}}
\end{picture}
