doc-src/System/Thy/document/Presentation.tex
changeset 34238 b28be884edda
parent 32088 2110fcd86efb
child 35587 f037aa6699c3
     1.1 --- a/doc-src/System/Thy/document/Presentation.tex	Sun Jan 03 15:09:02 2010 +0100
     1.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Mon Jan 04 11:55:23 2010 +0100
     1.3 @@ -485,7 +485,6 @@
     1.4    information (HTML etc.) according to settings.
     1.5  
     1.6    ISABELLE_USEDIR_OPTIONS=
     1.7 -  HOL_USEDIR_OPTIONS=
     1.8  
     1.9    ML_PLATFORM=x86-linux
    1.10    ML_HOME=/usr/local/polyml-5.2.1/x86-linux
    1.11 @@ -499,12 +498,7 @@
    1.12    distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} for the real
    1.13    work, one may control compilation options globally via above
    1.14    variable. In particular, generation of \rmindex{HTML} browsing
    1.15 -  information and document preparation is controlled here.
    1.16 -
    1.17 -  The \indexref{}{setting}{HOL\_USEDIR\_OPTIONS}\hyperlink{setting.HOL-USEDIR-OPTIONS}{\mbox{\isa{\isatt{HOL{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} setting is specific to the
    1.18 -  plain and main Isabelle/HOL images; its value is appended to
    1.19 -  \hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} for these particular sessions
    1.20 -  only.%
    1.21 +  information and document preparation is controlled here.%
    1.22  \end{isamarkuptext}%
    1.23  \isamarkuptrue%
    1.24  %