various tweaks to the HOL syntax and semantics

Use finite maps for the theory signature, to avoid the issue of
duplicate definitions. context_ok checks that the list of context
updates has no duplicates; to extract a signature from this list it is
turned into a finite map.

Also, give type abbreviations for various things that seem important:
assignments, valuations, signatures, interpretations... and clean up the
treatment of interpretations slightly.
some initial lemmas about the semantics

everything has become very context (signature) dependent. even though
the semantics aren't defined in terms of the signature, any proofs about
them require one to be around and the term/type to be good for that
signature. not sure if this is the right way to set things up...