mn200/HOL — pull request #178 by ptroja (2014-07-26 22:47:08+00:00)
Title: double 'the' removed

This patch removes double 'the' from both LaTeX documentation and ML comments.