--- a/doc-src/System/Thy/Presentation.thy Thu May 24 13:56:21 2012 +0200
+++ b/doc-src/System/Thy/Presentation.thy Thu May 24 14:46:14 2012 +0200
@@ -465,12 +465,12 @@
Build object-logic or run examples. Also creates browsing
information (HTML etc.) according to settings.
- ISABELLE_USEDIR_OPTIONS=
+ ISABELLE_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
+ ML_PLATFORM=...
+ ML_HOME=...
+ ML_SYSTEM=...
+ ML_OPTIONS=...
\end{ttbox}
Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
--- a/doc-src/System/Thy/document/Presentation.tex Thu May 24 13:56:21 2012 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Thu May 24 14:46:14 2012 +0200
@@ -491,12 +491,12 @@
Build object-logic or run examples. Also creates browsing
information (HTML etc.) according to settings.
- ISABELLE_USEDIR_OPTIONS=
+ ISABELLE_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
+ ML_PLATFORM=...
+ ML_HOME=...
+ ML_SYSTEM=...
+ ML_OPTIONS=...
\end{ttbox}
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}}}}