# HG changeset patch
# User wenzelm
# Date 1337863574 -7200
# Node ID f8f503a1782a383244c6f61297d81297507d5549
# Parent  455a9f89c47dffa43804d0cab59f379d117f93d4
less specific sample usage;

diff -r 455a9f89c47d -r f8f503a1782a doc-src/System/Thy/Presentation.thy
--- 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}
diff -r 455a9f89c47d -r f8f503a1782a doc-src/System/Thy/document/Presentation.tex
--- 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}}}}