--- a/Admin/CHECKLIST Thu Apr 02 14:39:29 2009 +0200
+++ b/Admin/CHECKLIST Thu Apr 02 14:49:58 2009 +0200
@@ -20,12 +20,9 @@
doc/Contents
- maintain Logics:
- Admin/makedist
build
lib/Tools/makeall
- lib/html/index.html
- doc-src/Logics/intro.tex
- doc-src/Logics/logics.tex
+ lib/html/library_index_content.template
- after release:
commit new ~isabelle/website/include/documentationdist.include.html to website SVN
--- a/INSTALL Thu Apr 02 14:39:29 2009 +0200
+++ b/INSTALL Thu Apr 02 14:49:58 2009 +0200
@@ -73,7 +73,7 @@
isabelle-process) directly from their location within the distribution
directory [ISABELLE_HOME] like this:
- [ISABELLE_HOME]/bin/isabelle-process HOL
+ [ISABELLE_HOME]/bin/isabelle tty -l HOL
This starts an interactive Isabelle session within the current text
terminal. [ISABELLE_HOME]/bin may be put into the shell's search
--- a/README Thu Apr 02 14:39:29 2009 +0200
+++ b/README Thu Apr 02 14:49:58 2009 +0200
@@ -11,7 +11,7 @@
Isabelle requires a regular Unix platform (e.g. GNU Linux) with the
following additional software:
- * A full Standard ML Compiler (works best with Poly/ML 5.x).
+ * A full Standard ML Compiler (works best with Poly/ML 5.2.1).
* The GNU bash shell (version 3.x or 2.x).
* Perl (version 5.x).
* GNU Emacs (version 21, 22) or XEmacs (version 21.4.x)
@@ -31,15 +31,12 @@
User interface
- The canonical Isabelle user interface is Proof General by David
- Aspinall and others. It is a generic (X)Emacs interface for proof
- assistants, including Isabelle. Proof General is suitable for use
- by pacifists and Emacs militants alike. Its most prominent feature
- is script management, providing a metaphor of live proof script
- editing.
-
- Proof General is distributed together with the XEmacs X-Symbol
- package, which provides a reasonable way to get proper mathematical
+ The main Isabelle user interface is Proof General by David Aspinall
+ and others. It is a generic Emacs interface for proof assistants,
+ including Isabelle. Proof General is suitable for use by pacifists
+ and Emacs militants alike. Its most prominent feature is script
+ management, providing a metaphor of live proof script editing.
+ Proof General also provides some support for proper mathematical
symbols displayed on screen.
Other sources of information
--- a/doc/Contents Thu Apr 02 14:39:29 2009 +0200
+++ b/doc/Contents Thu Apr 02 14:49:58 2009 +0200
@@ -13,7 +13,7 @@
implementation The Isabelle/Isar Implementation Manual
system The Isabelle System Manual
-Old Manuals (outdated!)
+Old Manuals (outdated)
intro Old Introduction to Isabelle
ref Old Isabelle Reference Manual
logics Isabelle's Logics: overview and misc logics
--- a/src/Pure/pure_thy.ML Thu Apr 02 14:39:29 2009 +0200
+++ b/src/Pure/pure_thy.ML Thu Apr 02 14:49:58 2009 +0200
@@ -31,10 +31,10 @@
val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
- val note_thmss: string -> (Thm.binding *
- (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
- val note_thmss_grouped: string -> string -> (Thm.binding *
- (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
+ val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
+ -> theory -> (string * thm list) list * theory
+ val note_thmss_grouped: string -> string -> (Thm.binding * (thm list * attribute list) list) list
+ -> theory -> (string * thm list) list * theory
val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
val add_defs: bool -> ((binding * term) * attribute list) list ->