Improve documentation on using assumptions.

Remove poor example of a database. Mention about using assumptions in Theories. Continuation of #857 with commits squashed.