Formalized Mathematics    (ISSN 1426-2630)
Volume 14, Number 2 (2006): PDF.

1. 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.

   ---

2. 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.

   ---