Update code base to use Theorem, Definition, Inductive, Type etc

[myreen]

The latest HOL has support for nice user facing syntax. This issue is about updating the entire code base to use the new syntax.

Two steps:

1. update all definitions, lemmas and theorems to use the new syntax
2. enforce the use of new syntax by making readme_gen reject old syntax.

Note that the updates need to be staged so that we don't create too much extra work on long running branches, such as words-bitwidth-semantics and ffi-ctypes. For example, I suspect we don't want to ban prove before those branches are merged into master or at least are closer to master.