doc-src/System/Thy/document/Presentation.tex

 
   Build object-logic or run examples. Also creates browsing
   information (HTML etc.) according to settings.
 
   ISABELLE_USEDIR_OPTIONS=
-  HOL_USEDIR_OPTIONS=
 
   ML_PLATFORM=x86-linux
   ML_HOME=/usr/local/polyml-5.2.1/x86-linux
   ML_SYSTEM=polyml-5.2.1
   ML_OPTIONS=-H 500

   setting is implicitly prefixed to \emph{any} \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}}
   call. Since the \verb|IsaMakefile|s of all object-logics
   distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} for the real
   work, one may control compilation options globally via above
   variable. In particular, generation of \rmindex{HTML} browsing
-  information and document preparation is controlled here.
-
-  The \indexref{}{setting}{HOL\_USEDIR\_OPTIONS}\hyperlink{setting.HOL-USEDIR-OPTIONS}{\mbox{\isa{\isatt{HOL{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} setting is specific to the
-  plain and main Isabelle/HOL images; its value is appended to
-  \hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} for these particular sessions
-  only.%
+  information and document preparation is controlled here.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsubsection{Options%
 }