@MISC{WSIERP_1.MIZ,
  AUTHOR = {Kondracki, Andrzej},
  TITLE = {The {C}hinese {R}emainder {T}heorem},
  DAY = {30},
  MONTH = {December},
  YEAR = {1997},
  ADDRESS1 = {AMS Management Systems Poland\\Warsaw},
  SUMMARY = {The article is a translation of the first chapters of a book {\em Wst{\Ple}p 
do teorii liczb} (Eng. {\em Introduction to Number Theory}) by W. Sierpi\'nski, WSiP,
Biblioteczka Matematyczna, Warszawa, 1987. The first few pages of this book 
have already
been formalized in MML. We prove the Chinese Remainder Theorem and Thue's
Theorem as well as several useful number theory propositions.}}

