translate tildes in EmitTeX strings

Made an new HOLTokenTilde command as the target. The default behaviour
of that command might be improved, but I don't know how (typesetting a
tilde nicely in TeX is apparently pretty hard...).