Start to refactor Sharing code

Change theory files to use an s-expression representation

This wastes some disk-space in the form of extra white-space that the
Oppen pretty-printer introduces for indentation purposes, but with the
string table used, the number of lines and the number of
non-whitespace characters is lower.

The string table can and will be used in more places in subsequent
commits to try to improve file size and sharing. The theory data may
also shift to directly use s-expressions rather than strings (people
wedded to a string representation can always embed those into
s-expressions of course).

Make further improvements to HOLsexp implementation

- install a pretty-printer for it in prelude
- provide a fromString implementation
- remove possible circularity in implementation's dependencies

Implement s-expression type for use in serialisation applications