380   %HOL-based theorem provers.

   380   %HOL-based theorem provers.

   381 

   381 

   382   Because of these problems to do with representing automata, formalising 

   382   Because of these problems to do with representing automata, formalising 

   383   automata theory is surprisingly not as easy as one might think, despite the 

   383   automata theory is surprisingly not as easy as one might think, despite the 

   384   sometimes very detailed, but informal, textbook proofs. \citeN{LammichTuerk12}

   384   sometimes very detailed, but informal, textbook proofs. \citeN{LammichTuerk12}

   386   Isabelle/HOL. There they use matrices for representing automata. 

   386   Isabelle/HOL. There they use matrices for representing automata. 

   387   Functions are used by \citeN{Nipkow98}, who establishes

   387   Functions are used by \citeN{Nipkow98}, who establishes

   388   the link between regular expressions and automata in the context of

   388   the link between regular expressions and automata in the context of

   389   lexing. \citeN{BerghoferReiter09} use functions as well for formalising automata

   389   lexing. \citeN{BerghoferReiter09} use functions as well for formalising automata

   390   working over bit strings in the context of Presburger arithmetic.  

   390   working over bit strings in the context of Presburger arithmetic.