misc updates for release;
authorwenzelm
Sun Jan 16 21:05:10 2011 +0100 (2011-01-16)
changeset 41596e424bc65080d
parent 41595 d0cced9cdeae
child 41597 ced4f78bb728
misc updates for release;
Admin/CHECKLIST
CONTRIBUTORS
README
doc/Contents
     1.1 --- a/Admin/CHECKLIST	Sun Jan 16 20:55:48 2011 +0100
     1.2 +++ b/Admin/CHECKLIST	Sun Jan 16 21:05:10 2011 +0100
     1.3 @@ -45,4 +45,3 @@
     1.4  - makebundle (multiplatform);
     1.5  
     1.6  - hdiutil create -srcfolder DIR DMG (Mac OS);
     1.7 -
     2.1 --- a/CONTRIBUTORS	Sun Jan 16 20:55:48 2011 +0100
     2.2 +++ b/CONTRIBUTORS	Sun Jan 16 21:05:10 2011 +0100
     2.3 @@ -20,20 +20,20 @@
     2.4    partial orders in HOL.
     2.5  
     2.6  * September 2010: Florian Haftmann, TUM
     2.7 -  Refined concepts for evaluation, i.e., normalisation of terms using
     2.8 +  Refined concepts for evaluation, i.e., normalization of terms using
     2.9    different techniques.
    2.10  
    2.11  * September 2010: Florian Haftmann, TUM
    2.12    Code generation for Scala.
    2.13  
    2.14  * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
    2.15 -  Rewriting the Probability theory.
    2.16 +  Improved Probability theory in HOL.
    2.17  
    2.18  * July 2010: Florian Haftmann, TUM
    2.19    Reworking and extension of the Imperative HOL framework.
    2.20  
    2.21 -* July 2010: Alexander Krauss, TUM and Christian Sternagel, University of
    2.22 -    Innsbruck
    2.23 +* July 2010: Alexander Krauss, TUM and Christian Sternagel, University
    2.24 +    of Innsbruck
    2.25    Ad-hoc overloading. Generic do notation for monads.
    2.26  
    2.27  
     3.1 --- a/README	Sun Jan 16 20:55:48 2011 +0100
     3.2 +++ b/README	Sun Jan 16 21:05:10 2011 +0100
     3.3 @@ -17,6 +17,7 @@
     3.4       * The GNU bash shell (version 3.x or 2.x).
     3.5       * Perl (version 5.x).
     3.6       * GNU Emacs (version 23) -- for the Proof General 4.x interface.
     3.7 +     * Java 1.6.x from Oracle/Sun or Apple -- for Scala and jEdit.
     3.8       * A complete LaTeX installation -- for document preparation.
     3.9  
    3.10  Installation
    3.11 @@ -31,11 +32,15 @@
    3.12  User interface
    3.13  
    3.14     The classic Isabelle user interface is Proof General by David
    3.15 -   Aspinall and others. It is a generic Emacs interface for proof
    3.16 +   Aspinall and others.  It is a generic Emacs interface for proof
    3.17     assistants, including Isabelle.  Its most prominent feature is
    3.18     script management, providing a metaphor of stepwise proof script
    3.19 -   editing.  Proof General also provides some support for mathematical
    3.20 -   symbols displayed on screen.
    3.21 +   editing.
    3.22 +
    3.23 +   Isabelle/jEdit is an experimental Prover IDE based on advanced
    3.24 +   technology of Isabelle/Scala.  It provides a metaphor of continuous
    3.25 +   proof checking of a versioned collection of theory sources, with
    3.26 +   instantaneous feedback in real-time.
    3.27  
    3.28  Other sources of information
    3.29  
     4.1 --- a/doc/Contents	Sun Jan 16 20:55:48 2011 +0100
     4.2 +++ b/doc/Contents	Sun Jan 16 21:05:10 2011 +0100
     4.3 @@ -10,7 +10,7 @@
     4.4    sledgehammer    User's Guide to Sledgehammer
     4.5    sugar           LaTeX Sugar for Isabelle documents
     4.6  
     4.7 -Reference Manuals
     4.8 +Main Reference Manuals
     4.9    isar-ref        The Isabelle/Isar Reference Manual
    4.10    implementation  The Isabelle/Isar Implementation Manual
    4.11    system          The Isabelle System Manual