This is a description of the theorem prover on an abstract level organized around data types. The order is top-down.
This is an older layer of documentation and its consistency with the remarks above may not be complete; it also may not refer to all commands referenced above. I will be working on remedying this.