--- 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
--- 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/
--- 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
--- 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 ***
--- 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
--- 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
--- 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"
--- 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>
--- 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. *}
--- 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."];
--- 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 ->