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.

[dnezam]

Fully updating to the new Quote syntax depends on https://github.com/HOL-Theorem-Prover/HOL/issues/1313 - in particular, there is at least once instance in characteristic/examples/cf_examplesScript.sml that is affected by this.

[dnezam]

Closing in favor of more specific issues such as #1263.