91   Science, with many beautiful theorems and many useful algorithms. There is a

    91   Science, with many beautiful theorems and many useful algorithms. There is a

    92   wide range of textbooks on this subject, many of which are aimed at students

    92   wide range of textbooks on this subject, many of which are aimed at students

    93   and contain very detailed `pencil-and-paper' proofs

    93   and contain very detailed `pencil-and-paper' proofs

    94   (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by

    94   (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by

    95   formalising the theorems and by verifying formally the algorithms.

    95   formalising the theorems and by verifying formally the algorithms.

    96 

    97 

    97   There is however a problem: the typical approach to regular languages is to

    98   There is however a problem: the typical approach to regular languages is to

    98   introduce finite automata and then define everything in terms of them.  For

    99   introduce finite automata and then define everything in terms of them.  For

    99   example, a regular language is normally defined as one whose strings are

   100   example, a regular language is normally defined as one whose strings are

   100   recognised by a finite deterministic automaton. This approach has many

   101   recognised by a finite deterministic automaton. This approach has many