Small changes to syntax hilight:
- recognize tokens (like "if" "then" "else") as symbols (instead of words);
- consider character "`" as generic string separator.
Improve syntax hilight using syntax-propertize-function.

Remove configuration for certain local variables (obsolete or not
appropriate): paragraph-start paragraph-separate require-final-newline
parse-sexp-ignore-comments.

Improve holl-send-tactic.

Use "hol_light" as default executable instead of "hol".