--- a/Admin/CHECKLIST Sun Jan 16 20:55:48 2011 +0100
+++ b/Admin/CHECKLIST Sun Jan 16 21:05:10 2011 +0100
@@ -45,4 +45,3 @@
- makebundle (multiplatform);
- hdiutil create -srcfolder DIR DMG (Mac OS);
-
--- a/CONTRIBUTORS Sun Jan 16 20:55:48 2011 +0100
+++ b/CONTRIBUTORS Sun Jan 16 21:05:10 2011 +0100
@@ -20,20 +20,20 @@
partial orders in HOL.
* September 2010: Florian Haftmann, TUM
- Refined concepts for evaluation, i.e., normalisation of terms using
+ Refined concepts for evaluation, i.e., normalization of terms using
different techniques.
* September 2010: Florian Haftmann, TUM
Code generation for Scala.
* August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
- Rewriting the Probability theory.
+ Improved Probability theory in HOL.
* July 2010: Florian Haftmann, TUM
Reworking and extension of the Imperative HOL framework.
-* July 2010: Alexander Krauss, TUM and Christian Sternagel, University of
- Innsbruck
+* July 2010: Alexander Krauss, TUM and Christian Sternagel, University
+ of Innsbruck
Ad-hoc overloading. Generic do notation for monads.
--- a/README Sun Jan 16 20:55:48 2011 +0100
+++ b/README Sun Jan 16 21:05:10 2011 +0100
@@ -17,6 +17,7 @@
* The GNU bash shell (version 3.x or 2.x).
* Perl (version 5.x).
* GNU Emacs (version 23) -- for the Proof General 4.x interface.
+ * Java 1.6.x from Oracle/Sun or Apple -- for Scala and jEdit.
* A complete LaTeX installation -- for document preparation.
Installation
@@ -31,11 +32,15 @@
User interface
The classic Isabelle user interface is Proof General by David
- Aspinall and others. It is a generic Emacs interface for proof
+ Aspinall and others. It is a generic Emacs interface for proof
assistants, including Isabelle. Its most prominent feature is
script management, providing a metaphor of stepwise proof script
- editing. Proof General also provides some support for mathematical
- symbols displayed on screen.
+ editing.
+
+ Isabelle/jEdit is an experimental Prover IDE based on advanced
+ technology of Isabelle/Scala. It provides a metaphor of continuous
+ proof checking of a versioned collection of theory sources, with
+ instantaneous feedback in real-time.
Other sources of information
--- a/doc/Contents Sun Jan 16 20:55:48 2011 +0100
+++ b/doc/Contents Sun Jan 16 21:05:10 2011 +0100
@@ -10,7 +10,7 @@
sledgehammer User's Guide to Sledgehammer
sugar LaTeX Sugar for Isabelle documents
-Reference Manuals
+Main Reference Manuals
isar-ref The Isabelle/Isar Reference Manual
implementation The Isabelle/Isar Implementation Manual
system The Isabelle System Manual