# HG changeset patch
# User wenzelm
# Date 1262602523 -3600
# Node ID b28be884eddad46c816d1484e537422ab4a70ff8
# Parent  225daff4323b7439602083a4e0be6dbfdfdcbe6f
discontinued special HOL_USEDIR_OPTIONS;

diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/annomaly
--- a/Admin/isatest/settings/annomaly	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/annomaly	Mon Jan 04 11:55:23 2010 +0100
@@ -24,5 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-HOL_USEDIR_OPTIONS="-p 0"
-
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/at-mac-poly-5.1-para
--- a/Admin/isatest/settings/at-mac-poly-5.1-para	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para	Mon Jan 04 11:55:23 2010 +0100
@@ -25,4 +25,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
 
-HOL_USEDIR_OPTIONS="-p 2 -q 0"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/at-poly
--- a/Admin/isatest/settings/at-poly	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/at-poly	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
 
-HOL_USEDIR_OPTIONS="-p 2"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/at-poly-5.1-para-e
--- a/Admin/isatest/settings/at-poly-5.1-para-e	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/at-poly-5.1-para-e	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 10"
 
-HOL_USEDIR_OPTIONS="-p 2 -q 0"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/at-poly-dev-e
--- a/Admin/isatest/settings/at-poly-dev-e	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/at-poly-dev-e	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-HOL_USEDIR_OPTIONS="-p 2"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/at-sml
--- a/Admin/isatest/settings/at-sml	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/at-sml	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-HOL_USEDIR_OPTIONS="-p 2"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/at-sml-dev-e
--- a/Admin/isatest/settings/at-sml-dev-e	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/at-sml-dev-e	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-HOL_USEDIR_OPTIONS="-p 0"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/at-sml-dev-p
--- a/Admin/isatest/settings/at-sml-dev-p	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/at-sml-dev-p	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-HOL_USEDIR_OPTIONS="-p 2"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/at64-poly
--- a/Admin/isatest/settings/at64-poly	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/at64-poly	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-HOL_USEDIR_OPTIONS="-p 2"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/at64-poly-5.1-para
--- a/Admin/isatest/settings/at64-poly-5.1-para	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/at64-poly-5.1-para	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 2"
 
-HOL_USEDIR_OPTIONS="-p 2 -q 0"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/at64-sml-dev
--- a/Admin/isatest/settings/at64-sml-dev	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/at64-sml-dev	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-HOL_USEDIR_OPTIONS="-p 2"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/mac-poly
--- a/Admin/isatest/settings/mac-poly	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/mac-poly	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -g false"
 
-HOL_USEDIR_OPTIONS="-p 2"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/mac-poly-M4
--- a/Admin/isatest/settings/mac-poly-M4	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/mac-poly-M4	Mon Jan 04 11:55:23 2010 +0100
@@ -25,4 +25,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
 
-HOL_USEDIR_OPTIONS="-p 2 -q 0"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/mac-poly-M8
--- a/Admin/isatest/settings/mac-poly-M8	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/mac-poly-M8	Mon Jan 04 11:55:23 2010 +0100
@@ -25,4 +25,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
 
-HOL_USEDIR_OPTIONS="-p 2 -q 0"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/mac-poly64-M4
--- a/Admin/isatest/settings/mac-poly64-M4	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/mac-poly64-M4	Mon Jan 04 11:55:23 2010 +0100
@@ -25,4 +25,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
 
-HOL_USEDIR_OPTIONS="-p 2 -q 2"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/mac-poly64-M8
--- a/Admin/isatest/settings/mac-poly64-M8	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/mac-poly64-M8	Mon Jan 04 11:55:23 2010 +0100
@@ -25,4 +25,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
 
-HOL_USEDIR_OPTIONS="-p 2 -q 2"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/mac-sml-dev
--- a/Admin/isatest/settings/mac-sml-dev	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/mac-sml-dev	Mon Jan 04 11:55:23 2010 +0100
@@ -24,4 +24,3 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-HOL_USEDIR_OPTIONS="-p 1"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/sun-poly
--- a/Admin/isatest/settings/sun-poly	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/sun-poly	Mon Jan 04 11:55:23 2010 +0100
@@ -25,4 +25,3 @@
 #ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true -M 6 -q 2"
 
-HOL_USEDIR_OPTIONS="-p 0" 
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/sun-sml
--- a/Admin/isatest/settings/sun-sml	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/sun-sml	Mon Jan 04 11:55:23 2010 +0100
@@ -25,4 +25,3 @@
 # ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-HOL_USEDIR_OPTIONS="-p 2"
diff -r 225daff4323b -r b28be884edda Admin/isatest/settings/sun-sml-dev
--- a/Admin/isatest/settings/sun-sml-dev	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/isatest/settings/sun-sml-dev	Mon Jan 04 11:55:23 2010 +0100
@@ -25,4 +25,3 @@
 # ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
 
-HOL_USEDIR_OPTIONS="-p 2"
diff -r 225daff4323b -r b28be884edda Admin/makebin
--- a/Admin/makebin	Sun Jan 03 15:09:02 2010 +0100
+++ b/Admin/makebin	Mon Jan 04 11:55:23 2010 +0100
@@ -88,7 +88,6 @@
 
 perl -pi \
   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \
-  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-M 1 -p 2":;' \
   etc/settings
 
 if [ -n "$DO_LIBRARY" ]; then
diff -r 225daff4323b -r b28be884edda NEWS
--- a/NEWS	Sun Jan 03 15:09:02 2010 +0100
+++ b/NEWS	Mon Jan 04 11:55:23 2010 +0100
@@ -48,6 +48,13 @@
 usual for resolution.  Rare INCOMPATIBILITY.
 
 
+*** System ***
+
+* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;
+ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that
+proof terms are enabled unconditionally in the new HOL-Proofs image.
+
+
 
 New in Isabelle2009-1 (December 2009)
 -------------------------------------
diff -r 225daff4323b -r b28be884edda build
--- a/build	Sun Jan 03 15:09:02 2010 +0100
+++ b/build	Mon Jan 04 11:55:23 2010 +0100
@@ -119,7 +119,6 @@
   echo "  ML_PLATFORM=$ML_PLATFORM"
   echo
   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
-  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
 fi
 
 
@@ -162,7 +161,6 @@
   echo "ML_PLATFORM=$ML_PLATFORM"
   echo
   echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
-  echo "HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
   echo
 fi
 
diff -r 225daff4323b -r b28be884edda doc-src/System/Thy/Presentation.thy
--- a/doc-src/System/Thy/Presentation.thy	Sun Jan 03 15:09:02 2010 +0100
+++ b/doc-src/System/Thy/Presentation.thy	Mon Jan 04 11:55:23 2010 +0100
@@ -459,7 +459,6 @@
   information (HTML etc.) according to settings.
 
   ISABELLE_USEDIR_OPTIONS=
-  HOL_USEDIR_OPTIONS=
 
   ML_PLATFORM=x86-linux
   ML_HOME=/usr/local/polyml-5.2.1/x86-linux
@@ -474,11 +473,6 @@
   work, one may control compilation options globally via above
   variable. In particular, generation of \rmindex{HTML} browsing
   information and document preparation is controlled here.
-
-  The @{setting_ref HOL_USEDIR_OPTIONS} setting is specific to the
-  plain and main Isabelle/HOL images; its value is appended to
-  @{setting ISABELLE_USEDIR_OPTIONS} for these particular sessions
-  only.
 *}
 
 
diff -r 225daff4323b -r b28be884edda doc-src/System/Thy/document/Presentation.tex
--- a/doc-src/System/Thy/document/Presentation.tex	Sun Jan 03 15:09:02 2010 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex	Mon Jan 04 11:55:23 2010 +0100
@@ -485,7 +485,6 @@
   information (HTML etc.) according to settings.
 
   ISABELLE_USEDIR_OPTIONS=
-  HOL_USEDIR_OPTIONS=
 
   ML_PLATFORM=x86-linux
   ML_HOME=/usr/local/polyml-5.2.1/x86-linux
@@ -499,12 +498,7 @@
   distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} for the real
   work, one may control compilation options globally via above
   variable. In particular, generation of \rmindex{HTML} browsing
-  information and document preparation is controlled here.
-
-  The \indexref{}{setting}{HOL\_USEDIR\_OPTIONS}\hyperlink{setting.HOL-USEDIR-OPTIONS}{\mbox{\isa{\isatt{HOL{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} setting is specific to the
-  plain and main Isabelle/HOL images; its value is appended to
-  \hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} for these particular sessions
-  only.%
+  information and document preparation is controlled here.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r 225daff4323b -r b28be884edda etc/settings
--- a/etc/settings	Sun Jan 03 15:09:02 2010 +0100
+++ b/etc/settings	Mon Jan 04 11:55:23 2010 +0100
@@ -89,10 +89,6 @@
 
 ISABELLE_USEDIR_OPTIONS="-M max -p 1 -q 2 -v true -V outline=/proof,/ML"
 
-# Specifically for the HOL image
-HOL_USEDIR_OPTIONS=""
-#HOL_USEDIR_OPTIONS="-p 2 -q 1"
-
 #Source file identification (default: full name + date stamp)
 ISABELLE_FILE_IDENT=""
 #ISABELLE_FILE_IDENT="md5"
diff -r 225daff4323b -r b28be884edda etc/user-settings.sample
--- a/etc/user-settings.sample	Sun Jan 03 15:09:02 2010 +0100
+++ b/etc/user-settings.sample	Mon Jan 04 11:55:23 2010 +0100
@@ -3,5 +3,4 @@
 # Isabelle user settings sample -- for use in ~/.isabelle/etc/settings
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
-HOL_USEDIR_OPTIONS="-p 1"
 ISABELLE_LOGIC=HOL
diff -r 225daff4323b -r b28be884edda lib/Tools/usedir
--- a/lib/Tools/usedir	Sun Jan 03 15:09:02 2010 +0100
+++ b/lib/Tools/usedir	Mon Jan 04 11:55:23 2010 +0100
@@ -38,7 +38,6 @@
   echo "  information (HTML etc.) according to settings."
   echo
   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
-  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
   echo
   echo "  ML_PLATFORM=$ML_PLATFORM"
   echo "  ML_HOME=$ML_HOME"