Isabelle is a great tool for automated theorem proving. I don’t need to tell you how great. It also comes with a great PDF generating tool which can help you create proof documents really easily. Here’s how you can create PDFs from your THY files:
http://recluzepage.googlepages.com/PdfFromThy.pdf