merged
authorwenzelm
Thu Apr 02 14:49:58 2009 +0200 (2009-04-02)
changeset 30854740517878d60
parent 30851 a218363290c3
parent 30853 6c6b7a72fa34
child 30855 c22436e6d350
merged
     1.1 --- a/Admin/CHECKLIST	Thu Apr 02 14:39:29 2009 +0200
     1.2 +++ b/Admin/CHECKLIST	Thu Apr 02 14:49:58 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:39:29 2009 +0200
     2.2 +++ b/INSTALL	Thu Apr 02 14:49:58 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:39:29 2009 +0200
     3.2 +++ b/README	Thu Apr 02 14:49:58 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:39:29 2009 +0200
     4.2 +++ b/doc/Contents	Thu Apr 02 14:49:58 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
     5.1 --- a/src/Pure/pure_thy.ML	Thu Apr 02 14:39:29 2009 +0200
     5.2 +++ b/src/Pure/pure_thy.ML	Thu Apr 02 14:49:58 2009 +0200
     5.3 @@ -31,10 +31,10 @@
     5.4    val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
     5.5    val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
     5.6    val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
     5.7 -  val note_thmss: string -> (Thm.binding *
     5.8 -      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
     5.9 -  val note_thmss_grouped: string -> string -> (Thm.binding *
    5.10 -      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
    5.11 +  val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list
    5.12 +    -> theory -> (string * thm list) list * theory
    5.13 +  val note_thmss_grouped: string -> string -> (Thm.binding * (thm list * attribute list) list) list
    5.14 +    -> theory -> (string * thm list) list * theory
    5.15    val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
    5.16    val add_axioms_cmd: ((binding * string) * attribute list) list -> theory -> thm list * theory
    5.17    val add_defs: bool -> ((binding * term) * attribute list) list ->