# HG changeset patch
# User berghofe
# Date 1238746146 -7200
# Node ID 294e8ee163ea37c0e0bacca81a80b5b369aaf6d2
# Parent  29eb80cef6b74f0f683c1876361312a554f30ec7# Parent  e5f9477aed50953d1009b01016bf2abb76066dfa
merged

diff -r e5f9477aed50 -r 294e8ee163ea Admin/CHECKLIST
--- a/Admin/CHECKLIST	Fri Apr 03 10:08:47 2009 +0200
+++ b/Admin/CHECKLIST	Fri Apr 03 10:09:06 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
diff -r e5f9477aed50 -r 294e8ee163ea Admin/makedist
--- a/Admin/makedist	Fri Apr 03 10:08:47 2009 +0200
+++ b/Admin/makedist	Fri Apr 03 10:09:06 2009 +0200
@@ -128,10 +128,9 @@
 # website
 
 mkdir -p ../website
-cat > ../website/distinfo.mak <<EOF
-# this is a generated file - do not edit unless you know what you are doing!
-DISTNAME=$DISTNAME
-DISTBASE=$DISTBASE
+cat > ../website/config <<EOF
+DISTNAME="$DISTNAME"
+DISTBASE="$DISTBASE"
 EOF
 
 cp lib/html/library_index_content.template ../website/
diff -r e5f9477aed50 -r 294e8ee163ea INSTALL
--- a/INSTALL	Fri Apr 03 10:08:47 2009 +0200
+++ b/INSTALL	Fri Apr 03 10:09:06 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
diff -r e5f9477aed50 -r 294e8ee163ea NEWS
--- a/NEWS	Fri Apr 03 10:08:47 2009 +0200
+++ b/NEWS	Fri Apr 03 10:09:06 2009 +0200
@@ -613,8 +613,36 @@
 
 *** HOL-Nominal ***
 
-* Modernized versions of commands 'nominal_inductive',
-'nominal_primrec', and 'equivariance' work with local theory targets.
+* Nominal datatypes can now contain type-variables.
+
+* Commands 'nominal_inductive' and 'equivariance' work with local
+theory targets.
+
+* Nominal primrec can now works with local theory targets and its
+specification syntax now conforms to the general format as seen in
+'inductive' etc.
+
+* Method "perm_simp" honours the standard simplifier attributes
+(no_asm), (no_asm_use) etc.
+
+* The new predicate #* is defined like freshness, except that on the
+left hand side can be a set or list of atoms.
+
+* Experimental command 'nominal_inductive2' derives strong induction
+principles for inductive definitions.  In contrast to
+'nominal_inductive', which can only deal with a fixed number of
+binders, it can deal with arbitrary expressions standing for sets of
+atoms to be avoided.  The only inductive definition we have at the
+moment that needs this generalisation is the typing rule for Lets in
+the algorithm W:
+
+ Gamma |- t1 : T1   (x,close Gamma T1)::Gamma |- t2 : T2   x#Gamma
+ -----------------------------------------------------------------
+         Gamma |- Let x be t1 in t2 : T2
+
+In this rule one wants to avoid all the binders that are introduced by
+"close Gamma T1".  We are looking for other examples where this
+feature might be useful.  Please let us know.
 
 
 *** HOLCF ***
@@ -630,8 +658,8 @@
 Potential INCOMPATIBILITY.
 
 * Command 'fixrec': specification syntax now conforms to the general
-format as seen in 'inductive', 'primrec', 'function', etc.  See
-src/HOLCF/ex/Fixrec_ex.thy for examples.  INCOMPATIBILITY.
+format as seen in 'inductive' etc.  See src/HOLCF/ex/Fixrec_ex.thy for
+examples.  INCOMPATIBILITY.
 
 
 *** ZF ***
diff -r e5f9477aed50 -r 294e8ee163ea README
--- a/README	Fri Apr 03 10:08:47 2009 +0200
+++ b/README	Fri Apr 03 10:09:06 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
diff -r e5f9477aed50 -r 294e8ee163ea doc/Contents
--- a/doc/Contents	Fri Apr 03 10:08:47 2009 +0200
+++ b/doc/Contents	Fri Apr 03 10:09:06 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
diff -r e5f9477aed50 -r 294e8ee163ea etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Apr 03 10:08:47 2009 +0200
+++ b/etc/isar-keywords.el	Fri Apr 03 10:09:06 2009 +0200
@@ -291,7 +291,6 @@
     "notes"
     "obtains"
     "open"
-    "otherwise"
     "output"
     "outputs"
     "overloaded"
diff -r e5f9477aed50 -r 294e8ee163ea lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Fri Apr 03 10:08:47 2009 +0200
+++ b/lib/jedit/isabelle.xml	Fri Apr 03 10:09:06 2009 +0200
@@ -212,7 +212,6 @@
       <OPERATOR>oops</OPERATOR>
       <KEYWORD4>open</KEYWORD4>
       <OPERATOR>oracle</OPERATOR>
-      <KEYWORD4>otherwise</KEYWORD4>
       <KEYWORD4>output</KEYWORD4>
       <KEYWORD4>outputs</KEYWORD4>
       <KEYWORD4>overloaded</KEYWORD4>
diff -r e5f9477aed50 -r 294e8ee163ea src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Apr 03 10:08:47 2009 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Apr 03 10:09:06 2009 +0200
@@ -1216,6 +1216,14 @@
     "finite F ==> (setsum f F = 0) = (ALL a:F. f a = (0::nat))"
 by (induct set: finite) auto
 
+lemma setsum_eq_Suc0_iff: "finite A \<Longrightarrow>
+  (setsum f A = Suc 0) = (EX a:A. f a = Suc 0 & (ALL b:A. a\<noteq>b \<longrightarrow> f b = 0))"
+apply(erule finite_induct)
+apply (auto simp add:add_is_1)
+done
+
+lemmas setsum_eq_1_iff = setsum_eq_Suc0_iff[simplified One_nat_def[symmetric]]
+
 lemma setsum_Un_nat: "finite A ==> finite B ==>
   (setsum f (A Un B) :: nat) = setsum f A + setsum f B - setsum f (A Int B)"
   -- {* For the natural numbers, we have subtraction. *}
diff -r e5f9477aed50 -r 294e8ee163ea src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Fri Apr 03 10:08:47 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Fri Apr 03 10:09:06 2009 +0200
@@ -459,7 +459,7 @@
     
   (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
   
-  val failure_strings_E = ["SZS status: Satisfiable","SZS status: ResourceOut","# Cannot determine problem status"];
+  val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable","SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
   val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
   val failure_strings_SPASS = ["SPASS beiseite: Completion found.","SPASS beiseite: Ran out of time.",
   "SPASS beiseite: Maximal number of loops exceeded."];
diff -r e5f9477aed50 -r 294e8ee163ea src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Apr 03 10:08:47 2009 +0200
+++ b/src/Pure/pure_thy.ML	Fri Apr 03 10:09:06 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 ->