less specific sample usage;
authorwenzelm
Thu, 24 May 2012 14:46:14 +0200
changeset 48993f8f503a1782a
parent 48992 455a9f89c47d
child 48994 59ec72d3d0b9
less specific sample usage;
doc-src/System/Thy/Presentation.thy
doc-src/System/Thy/document/Presentation.tex
     1.1 --- a/doc-src/System/Thy/Presentation.thy	Thu May 24 13:56:21 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Presentation.thy	Thu May 24 14:46:14 2012 +0200
     1.3 @@ -465,12 +465,12 @@
     1.4    Build object-logic or run examples. Also creates browsing
     1.5    information (HTML etc.) according to settings.
     1.6  
     1.7 -  ISABELLE_USEDIR_OPTIONS=
     1.8 +  ISABELLE_USEDIR_OPTIONS=...
     1.9  
    1.10 -  ML_PLATFORM=x86-linux
    1.11 -  ML_HOME=/usr/local/polyml-5.2.1/x86-linux
    1.12 -  ML_SYSTEM=polyml-5.2.1
    1.13 -  ML_OPTIONS=-H 500
    1.14 +  ML_PLATFORM=...
    1.15 +  ML_HOME=...
    1.16 +  ML_SYSTEM=...
    1.17 +  ML_OPTIONS=...
    1.18  \end{ttbox}
    1.19  
    1.20    Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
     2.1 --- a/doc-src/System/Thy/document/Presentation.tex	Thu May 24 13:56:21 2012 +0200
     2.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Thu May 24 14:46:14 2012 +0200
     2.3 @@ -491,12 +491,12 @@
     2.4    Build object-logic or run examples. Also creates browsing
     2.5    information (HTML etc.) according to settings.
     2.6  
     2.7 -  ISABELLE_USEDIR_OPTIONS=
     2.8 +  ISABELLE_USEDIR_OPTIONS=...
     2.9  
    2.10 -  ML_PLATFORM=x86-linux
    2.11 -  ML_HOME=/usr/local/polyml-5.2.1/x86-linux
    2.12 -  ML_SYSTEM=polyml-5.2.1
    2.13 -  ML_OPTIONS=-H 500
    2.14 +  ML_PLATFORM=...
    2.15 +  ML_HOME=...
    2.16 +  ML_SYSTEM=...
    2.17 +  ML_OPTIONS=...
    2.18  \end{ttbox}
    2.19  
    2.20    Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}