A copy of this issue can also be found on the
MetaPress server (with DOI names of articles).
Marco Riccardi.
Pocklington's Theorem and Bertrand's Postulate,
Formalized Mathematics 14(2), pages 47-52, 2006. MML Identifier: NAT_4 Summary: The first four sections include some auxiliary theorems related to number and finite sequence of numbers, in particular a primality test, the Pocklington's theorem (see \cite{LeVeque}). The last section presents the formalization of Bertrand's postulate closely following the book \cite{PFTB}, pp. 7--9.
Noboru Endou, Yasunari Shidama.
Integral of Measurable Function,
Formalized Mathematics 14(2), pages 53-70, 2006. MML Identifier: MESFUNC5 Summary: In this paper we construct integral of measurable function.