better match intended semantics of OpenTheory names

rather than using strings, now have a type abbreviation otname for
string list * string. it might be worth writing more operations on this
type (like for manipulating the namespace).

functions from thy_{const,tyop} to string in OpenTheoryCommon

translation to and from opentheory type variable names

Implement 10 more inference rules on OpenTheory kernel

Also rewrite MP, because previous code was likely to loop.
20 rules to go.

start work on log_thm

Contrary to the initial plan of having an intermediate extended article
file format, it seems feasible to do the compilation to the OpenTheory
virtual machine on the fly. Being outside of the kernel (and thus in the
scope of boolTheory, Drule, etc.) makes this possible. However, we must
be careful to avoid implementing an inference rule in terms of itself
(and thus sending log_thm into a loop).

SUBST is the first rule to pose a challenge (and probably won't be
the last), so I've left it for now. Next step is probably to get rid of
TODO_prf (by adding proof cases for the remaining rules in Thm).

logging facility work in progress (terms, but not yet theorems)