--- a/Journal/Paper.thy	Fri Jun 03 13:59:21 2011 +0000
+++ b/Journal/Paper.thy	Mon Jul 25 13:33:38 2011 +0000
@@ -93,6 +93,7 @@
   and contain very detailed `pencil-and-paper' proofs
   (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by
   formalising the theorems and by verifying formally the algorithms.
+  Some of the popular theorem provers are based on Higher-Order Logic (HOL).
 
   There is however a problem: the typical approach to regular languages is to
   introduce finite automata and then define everything in terms of them.  For