## Automata Library

Aleksey Nogin took the original automata library and removed unnecessary exponentials from the proof of Myhill - Nerode theorem (see his technical report for more information).
- The following theories have been changed (Nuprl 4.2)
- The following theories were left unchanged (Nuprl 4.2b, may be incompatible with Nuprl 4.2)