doc-src/System/Thy/document/Presentation.tex
changeset 47978 f8f503a1782a
parent 43564 9864182c6bad
child 48576 72c0bf1f544f
--- 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}}}}