misc tuning for release;
authorwenzelm
Thu Apr 02 14:30:16 2009 +0200 (2009-04-02)
changeset 3085259a422908e29
parent 30849 0e5ec6d2c1d9
child 30853 6c6b7a72fa34
misc tuning for release;
Admin/CHECKLIST
INSTALL
README
doc/Contents
     1.1 --- a/Admin/CHECKLIST	Thu Apr 02 14:09:41 2009 +0200
     1.2 +++ b/Admin/CHECKLIST	Thu Apr 02 14:30:16 2009 +0200
     1.3 @@ -20,12 +20,9 @@
     1.4      doc/Contents
     1.5  
     1.6  - maintain Logics:
     1.7 -    Admin/makedist
     1.8      build
     1.9      lib/Tools/makeall
    1.10 -    lib/html/index.html
    1.11 -    doc-src/Logics/intro.tex
    1.12 -    doc-src/Logics/logics.tex
    1.13 +    lib/html/library_index_content.template
    1.14  
    1.15  - after release: 
    1.16      commit new ~isabelle/website/include/documentationdist.include.html to website SVN
     2.1 --- a/INSTALL	Thu Apr 02 14:09:41 2009 +0200
     2.2 +++ b/INSTALL	Thu Apr 02 14:30:16 2009 +0200
     2.3 @@ -73,7 +73,7 @@
     2.4  isabelle-process) directly from their location within the distribution
     2.5  directory [ISABELLE_HOME] like this:
     2.6  
     2.7 -  [ISABELLE_HOME]/bin/isabelle-process HOL
     2.8 +  [ISABELLE_HOME]/bin/isabelle tty -l HOL
     2.9  
    2.10  This starts an interactive Isabelle session within the current text
    2.11  terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
     3.1 --- a/README	Thu Apr 02 14:09:41 2009 +0200
     3.2 +++ b/README	Thu Apr 02 14:30:16 2009 +0200
     3.3 @@ -11,7 +11,7 @@
     3.4  
     3.5     Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
     3.6     following additional software:
     3.7 -     * A full Standard ML Compiler (works best with Poly/ML 5.x).
     3.8 +     * A full Standard ML Compiler (works best with Poly/ML 5.2.1).
     3.9       * The GNU bash shell (version 3.x or 2.x).
    3.10       * Perl (version 5.x).
    3.11       * GNU Emacs (version 21, 22) or XEmacs (version 21.4.x)
    3.12 @@ -31,15 +31,12 @@
    3.13  
    3.14  User interface
    3.15  
    3.16 -   The canonical Isabelle user interface is Proof General by David
    3.17 -   Aspinall and others. It is a generic (X)Emacs interface for proof
    3.18 -   assistants, including Isabelle. Proof General is suitable for use
    3.19 -   by pacifists and Emacs militants alike. Its most prominent feature
    3.20 -   is script management, providing a metaphor of live proof script
    3.21 -   editing.
    3.22 -
    3.23 -   Proof General is distributed together with the XEmacs X-Symbol
    3.24 -   package, which provides a reasonable way to get proper mathematical
    3.25 +   The main Isabelle user interface is Proof General by David Aspinall
    3.26 +   and others. It is a generic Emacs interface for proof assistants,
    3.27 +   including Isabelle. Proof General is suitable for use by pacifists
    3.28 +   and Emacs militants alike. Its most prominent feature is script
    3.29 +   management, providing a metaphor of live proof script editing.
    3.30 +   Proof General also provides some support for proper mathematical
    3.31     symbols displayed on screen.
    3.32  
    3.33  Other sources of information
     4.1 --- a/doc/Contents	Thu Apr 02 14:09:41 2009 +0200
     4.2 +++ b/doc/Contents	Thu Apr 02 14:30:16 2009 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4    implementation  The Isabelle/Isar Implementation Manual
     4.5    system          The Isabelle System Manual
     4.6  
     4.7 -Old Manuals (outdated!)
     4.8 +Old Manuals (outdated)
     4.9    intro           Old Introduction to Isabelle
    4.10    ref             Old Isabelle Reference Manual
    4.11    logics          Isabelle's Logics: overview and misc logics