* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image; ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions. Note that proof terms are enabled unconditionally in the new HOL-Proofs image. Makarius