The files here are described on the Metamath Home Page at http://metamath.org .