--- 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"
-
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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"
--- 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
--- 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)
-------------------------------------
--- 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
--- 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.
*}
--- 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%
%
--- 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"
--- 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
--- 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"