Store "local" theorems (e.g., with Triviality) in DB

The reverse lookup now returns the list of "locations" where a theorem
is available.

Install a reverse lookup facility in DB

Extend DB; find recognises cool op'ns in strings; add selectDB

1. Arguments to find and find_in can now use | and ~ operators. They
are union and intersection. (Am strongly thinking of changing ~ to
&.) The union is weaker in precedence. There are no parentheses
because nested unions are easier to achieve by just chaining
queries.

2. The new selectDB entrypoint allows for chaining of match, find and
selecting-by-theory queries. "Chaining" = intersection. Previously,
this effect had to be achieved with DB.match/find followed by calls
to find_in and apropos_in. Now there's just one list argument with
special constructors.

The emacs mode supports writing these lists with M-h M.

Remove unused CT from DB.sig (it's used internally but not elsewhere)

Get more regression tests to pass in theoryIO branch