1.1 --- a/Admin/isatest/settings/annomaly	Sun Jan 03 15:09:02 2010 +0100
     1.2 +++ b/Admin/isatest/settings/annomaly	Mon Jan 04 11:55:23 2010 +0100
     1.3 @@ -24,5 +24,3 @@
     1.4  
     1.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
     1.6  
     1.7 -HOL_USEDIR_OPTIONS="-p 0"
     1.8 -

     2.1 --- a/Admin/isatest/settings/at-mac-poly-5.1-para	Sun Jan 03 15:09:02 2010 +0100
     2.2 +++ b/Admin/isatest/settings/at-mac-poly-5.1-para	Mon Jan 04 11:55:23 2010 +0100
     2.3 @@ -25,4 +25,3 @@
     2.4  
     2.5  ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
     2.6  
     2.7 -HOL_USEDIR_OPTIONS="-p 2 -q 0"

     3.1 --- a/Admin/isatest/settings/at-poly	Sun Jan 03 15:09:02 2010 +0100
     3.2 +++ b/Admin/isatest/settings/at-poly	Mon Jan 04 11:55:23 2010 +0100
     3.3 @@ -24,4 +24,3 @@
     3.4  
     3.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
     3.6  
     3.7 -HOL_USEDIR_OPTIONS="-p 2"

     4.1 --- a/Admin/isatest/settings/at-poly-5.1-para-e	Sun Jan 03 15:09:02 2010 +0100
     4.2 +++ b/Admin/isatest/settings/at-poly-5.1-para-e	Mon Jan 04 11:55:23 2010 +0100
     4.3 @@ -24,4 +24,3 @@
     4.4  
     4.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 10"
     4.6  
     4.7 -HOL_USEDIR_OPTIONS="-p 2 -q 0"

     5.1 --- a/Admin/isatest/settings/at-poly-dev-e	Sun Jan 03 15:09:02 2010 +0100
     5.2 +++ b/Admin/isatest/settings/at-poly-dev-e	Mon Jan 04 11:55:23 2010 +0100
     5.3 @@ -24,4 +24,3 @@
     5.4  
     5.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
     5.6  
     5.7 -HOL_USEDIR_OPTIONS="-p 2"

     6.1 --- a/Admin/isatest/settings/at-sml	Sun Jan 03 15:09:02 2010 +0100
     6.2 +++ b/Admin/isatest/settings/at-sml	Mon Jan 04 11:55:23 2010 +0100
     6.3 @@ -24,4 +24,3 @@
     6.4  
     6.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
     6.6  
     6.7 -HOL_USEDIR_OPTIONS="-p 2"

     7.1 --- a/Admin/isatest/settings/at-sml-dev-e	Sun Jan 03 15:09:02 2010 +0100
     7.2 +++ b/Admin/isatest/settings/at-sml-dev-e	Mon Jan 04 11:55:23 2010 +0100
     7.3 @@ -24,4 +24,3 @@
     7.4  
     7.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
     7.6  
     7.7 -HOL_USEDIR_OPTIONS="-p 0"

     8.1 --- a/Admin/isatest/settings/at-sml-dev-p	Sun Jan 03 15:09:02 2010 +0100
     8.2 +++ b/Admin/isatest/settings/at-sml-dev-p	Mon Jan 04 11:55:23 2010 +0100
     8.3 @@ -24,4 +24,3 @@
     8.4  
     8.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
     8.6  
     8.7 -HOL_USEDIR_OPTIONS="-p 2"

     9.1 --- a/Admin/isatest/settings/at64-poly	Sun Jan 03 15:09:02 2010 +0100
     9.2 +++ b/Admin/isatest/settings/at64-poly	Mon Jan 04 11:55:23 2010 +0100
     9.3 @@ -24,4 +24,3 @@
     9.4  
     9.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
     9.6  
     9.7 -HOL_USEDIR_OPTIONS="-p 2"

    10.1 --- a/Admin/isatest/settings/at64-poly-5.1-para	Sun Jan 03 15:09:02 2010 +0100
    10.2 +++ b/Admin/isatest/settings/at64-poly-5.1-para	Mon Jan 04 11:55:23 2010 +0100
    10.3 @@ -24,4 +24,3 @@
    10.4  
    10.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 2"
    10.6  
    10.7 -HOL_USEDIR_OPTIONS="-p 2 -q 0"

    11.1 --- a/Admin/isatest/settings/at64-sml-dev	Sun Jan 03 15:09:02 2010 +0100
    11.2 +++ b/Admin/isatest/settings/at64-sml-dev	Mon Jan 04 11:55:23 2010 +0100
    11.3 @@ -24,4 +24,3 @@
    11.4  
    11.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
    11.6  
    11.7 -HOL_USEDIR_OPTIONS="-p 2"

    12.1 --- a/Admin/isatest/settings/mac-poly	Sun Jan 03 15:09:02 2010 +0100
    12.2 +++ b/Admin/isatest/settings/mac-poly	Mon Jan 04 11:55:23 2010 +0100
    12.3 @@ -24,4 +24,3 @@
    12.4  
    12.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -g false"
    12.6  
    12.7 -HOL_USEDIR_OPTIONS="-p 2"

    13.1 --- a/Admin/isatest/settings/mac-poly-M4	Sun Jan 03 15:09:02 2010 +0100
    13.2 +++ b/Admin/isatest/settings/mac-poly-M4	Mon Jan 04 11:55:23 2010 +0100
    13.3 @@ -25,4 +25,3 @@
    13.4  
    13.5  ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
    13.6  
    13.7 -HOL_USEDIR_OPTIONS="-p 2 -q 0"

    14.1 --- a/Admin/isatest/settings/mac-poly-M8	Sun Jan 03 15:09:02 2010 +0100
    14.2 +++ b/Admin/isatest/settings/mac-poly-M8	Mon Jan 04 11:55:23 2010 +0100
    14.3 @@ -25,4 +25,3 @@
    14.4  
    14.5  ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
    14.6  
    14.7 -HOL_USEDIR_OPTIONS="-p 2 -q 0"

    15.1 --- a/Admin/isatest/settings/mac-poly64-M4	Sun Jan 03 15:09:02 2010 +0100
    15.2 +++ b/Admin/isatest/settings/mac-poly64-M4	Mon Jan 04 11:55:23 2010 +0100
    15.3 @@ -25,4 +25,3 @@
    15.4  
    15.5  ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 4 -q 2"
    15.6  
    15.7 -HOL_USEDIR_OPTIONS="-p 2 -q 2"

    16.1 --- a/Admin/isatest/settings/mac-poly64-M8	Sun Jan 03 15:09:02 2010 +0100
    16.2 +++ b/Admin/isatest/settings/mac-poly64-M8	Mon Jan 04 11:55:23 2010 +0100
    16.3 @@ -25,4 +25,3 @@
    16.4  
    16.5  ISABELLE_USEDIR_OPTIONS="-i false -d false -t true -M 8 -q 2"
    16.6  
    16.7 -HOL_USEDIR_OPTIONS="-p 2 -q 2"

    17.1 --- a/Admin/isatest/settings/mac-sml-dev	Sun Jan 03 15:09:02 2010 +0100
    17.2 +++ b/Admin/isatest/settings/mac-sml-dev	Mon Jan 04 11:55:23 2010 +0100
    17.3 @@ -24,4 +24,3 @@
    17.4  
    17.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
    17.6  
    17.7 -HOL_USEDIR_OPTIONS="-p 1"

    18.1 --- a/Admin/isatest/settings/sun-poly	Sun Jan 03 15:09:02 2010 +0100
    18.2 +++ b/Admin/isatest/settings/sun-poly	Mon Jan 04 11:55:23 2010 +0100
    18.3 @@ -25,4 +25,3 @@
    18.4  #ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
    18.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true -M 6 -q 2"
    18.6  
    18.7 -HOL_USEDIR_OPTIONS="-p 0" 

    19.1 --- a/Admin/isatest/settings/sun-sml	Sun Jan 03 15:09:02 2010 +0100
    19.2 +++ b/Admin/isatest/settings/sun-sml	Mon Jan 04 11:55:23 2010 +0100
    19.3 @@ -25,4 +25,3 @@
    19.4  # ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
    19.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
    19.6  
    19.7 -HOL_USEDIR_OPTIONS="-p 2"

    20.1 --- a/Admin/isatest/settings/sun-sml-dev	Sun Jan 03 15:09:02 2010 +0100
    20.2 +++ b/Admin/isatest/settings/sun-sml-dev	Mon Jan 04 11:55:23 2010 +0100
    20.3 @@ -25,4 +25,3 @@
    20.4  # ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
    20.5  ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
    20.6  
    20.7 -HOL_USEDIR_OPTIONS="-p 2"

    21.1 --- a/Admin/makebin	Sun Jan 03 15:09:02 2010 +0100
    21.2 +++ b/Admin/makebin	Mon Jan 04 11:55:23 2010 +0100
    21.3 @@ -88,7 +88,6 @@
    21.4  
    21.5  perl -pi \
    21.6    -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \
    21.7 -  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-M 1 -p 2":;' \
    21.8    etc/settings
    21.9  
   21.10  if [ -n "$DO_LIBRARY" ]; then

    22.1 --- a/NEWS	Sun Jan 03 15:09:02 2010 +0100
    22.2 +++ b/NEWS	Mon Jan 04 11:55:23 2010 +0100
    22.3 @@ -48,6 +48,13 @@
    22.4  usual for resolution.  Rare INCOMPATIBILITY.
    22.5  
    22.6  
    22.7 +*** System ***
    22.8 +
    22.9 +* Discontinued special HOL_USEDIR_OPTIONS for the main HOL image;
   22.10 +ISABELLE_USEDIR_OPTIONS applies uniformly to all sessions.  Note that
   22.11 +proof terms are enabled unconditionally in the new HOL-Proofs image.
   22.12 +
   22.13 +
   22.14  
   22.15  New in Isabelle2009-1 (December 2009)
   22.16  -------------------------------------

    23.1 --- a/build	Sun Jan 03 15:09:02 2010 +0100
    23.2 +++ b/build	Mon Jan 04 11:55:23 2010 +0100
    23.3 @@ -119,7 +119,6 @@
    23.4    echo "  ML_PLATFORM=$ML_PLATFORM"
    23.5    echo
    23.6    echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
    23.7 -  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
    23.8  fi
    23.9  
   23.10  
   23.11 @@ -162,7 +161,6 @@
   23.12    echo "ML_PLATFORM=$ML_PLATFORM"
   23.13    echo
   23.14    echo "ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   23.15 -  echo "HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
   23.16    echo
   23.17  fi
   23.18  

    24.1 --- a/doc-src/System/Thy/Presentation.thy	Sun Jan 03 15:09:02 2010 +0100
    24.2 +++ b/doc-src/System/Thy/Presentation.thy	Mon Jan 04 11:55:23 2010 +0100
    24.3 @@ -459,7 +459,6 @@
    24.4    information (HTML etc.) according to settings.
    24.5  
    24.6    ISABELLE_USEDIR_OPTIONS=
    24.7 -  HOL_USEDIR_OPTIONS=
    24.8  
    24.9    ML_PLATFORM=x86-linux
   24.10    ML_HOME=/usr/local/polyml-5.2.1/x86-linux
   24.11 @@ -474,11 +473,6 @@
   24.12    work, one may control compilation options globally via above
   24.13    variable. In particular, generation of \rmindex{HTML} browsing
   24.14    information and document preparation is controlled here.
   24.15 -
   24.16 -  The @{setting_ref HOL_USEDIR_OPTIONS} setting is specific to the
   24.17 -  plain and main Isabelle/HOL images; its value is appended to
   24.18 -  @{setting ISABELLE_USEDIR_OPTIONS} for these particular sessions
   24.19 -  only.
   24.20  *}
   24.21  
   24.22  

    25.1 --- a/doc-src/System/Thy/document/Presentation.tex	Sun Jan 03 15:09:02 2010 +0100
    25.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Mon Jan 04 11:55:23 2010 +0100
    25.3 @@ -485,7 +485,6 @@
    25.4    information (HTML etc.) according to settings.
    25.5  
    25.6    ISABELLE_USEDIR_OPTIONS=
    25.7 -  HOL_USEDIR_OPTIONS=
    25.8  
    25.9    ML_PLATFORM=x86-linux
   25.10    ML_HOME=/usr/local/polyml-5.2.1/x86-linux
   25.11 @@ -499,12 +498,7 @@
   25.12    distributed with Isabelle just invoke \hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} for the real
   25.13    work, one may control compilation options globally via above
   25.14    variable. In particular, generation of \rmindex{HTML} browsing
   25.15 -  information and document preparation is controlled here.
   25.16 -
   25.17 -  The \indexref{}{setting}{HOL\_USEDIR\_OPTIONS}\hyperlink{setting.HOL-USEDIR-OPTIONS}{\mbox{\isa{\isatt{HOL{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} setting is specific to the
   25.18 -  plain and main Isabelle/HOL images; its value is appended to
   25.19 -  \hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}USEDIR{\isacharunderscore}OPTIONS}}}} for these particular sessions
   25.20 -  only.%
   25.21 +  information and document preparation is controlled here.%
   25.22  \end{isamarkuptext}%
   25.23  \isamarkuptrue%
   25.24  %

    26.1 --- a/etc/settings	Sun Jan 03 15:09:02 2010 +0100
    26.2 +++ b/etc/settings	Mon Jan 04 11:55:23 2010 +0100
    26.3 @@ -89,10 +89,6 @@
    26.4  
    26.5  ISABELLE_USEDIR_OPTIONS="-M max -p 1 -q 2 -v true -V outline=/proof,/ML"
    26.6  
    26.7 -# Specifically for the HOL image
    26.8 -HOL_USEDIR_OPTIONS=""
    26.9 -#HOL_USEDIR_OPTIONS="-p 2 -q 1"
   26.10 -
   26.11  #Source file identification (default: full name + date stamp)
   26.12  ISABELLE_FILE_IDENT=""
   26.13  #ISABELLE_FILE_IDENT="md5"

    27.1 --- a/etc/user-settings.sample	Sun Jan 03 15:09:02 2010 +0100
    27.2 +++ b/etc/user-settings.sample	Mon Jan 04 11:55:23 2010 +0100
    27.3 @@ -3,5 +3,4 @@
    27.4  # Isabelle user settings sample -- for use in ~/.isabelle/etc/settings
    27.5  
    27.6  ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
    27.7 -HOL_USEDIR_OPTIONS="-p 1"
    27.8  ISABELLE_LOGIC=HOL

    28.1 --- a/lib/Tools/usedir	Sun Jan 03 15:09:02 2010 +0100
    28.2 +++ b/lib/Tools/usedir	Mon Jan 04 11:55:23 2010 +0100
    28.3 @@ -38,7 +38,6 @@
    28.4    echo "  information (HTML etc.) according to settings."
    28.5    echo
    28.6    echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
    28.7 -  echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
    28.8    echo
    28.9    echo "  ML_PLATFORM=$ML_PLATFORM"
   28.10    echo "  ML_HOME=$ML_HOME"