--- a/CONTRIBUTORS Sun Nov 22 14:13:18 2009 +0100
+++ b/CONTRIBUTORS Sun Nov 22 14:49:36 2009 +0100
@@ -15,7 +15,7 @@
* November 2009: Lukas Bulwahn, TUM
Predicate Compiler: a compiler for inductive predicates to
- equational specfications.
+ equational specifications.
* November 2009: Sascha Boehme, TUM
HOL-Boogie: an interactive prover back-end for Boogie and VCC.
@@ -56,11 +56,11 @@
for code generation.
* June 2009: Florian Haftmann, TUM
- HOL/Library/Tree: searchtrees implementing mappings, ready to use
+ HOL/Library/Tree: search trees implementing mappings, ready to use
for code generation.
* March 2009: Philipp Meyer, TUM
- Minimalization algorithm for results from sledgehammer call.
+ Minimization tool for results from Sledgehammer.
Contributions to Isabelle2009
--- a/NEWS Sun Nov 22 14:13:18 2009 +0100
+++ b/NEWS Sun Nov 22 14:49:36 2009 +0100
@@ -12,9 +12,6 @@
*** Pure ***
-* On instantiation of classes, remaining undefined class parameters
-are formally declared. INCOMPATIBILITY.
-
* Locale interpretation propagates mixins along the locale hierarchy.
The currently only available mixins are the equations used to map
local definitions to terms of the target domain of an interpretation.
@@ -26,6 +23,9 @@
* Thoroughly revised locales tutorial. New section on conditional
interpretation.
+* On instantiation of classes, remaining undefined class parameters
+are formally declared. INCOMPATIBILITY.
+
*** Document preparation ***
@@ -37,19 +37,6 @@
*** HOL ***
-* A tabled implementation of the reflexive transitive closure.
-
-* New commands 'code_pred' and 'values' to invoke the predicate
-compiler and to enumerate values of inductive predicates.
-
-* Combined former theories Divides and IntDiv to one theory Divides in
-the spirit of other number theory theories in HOL; some constants (and
-to a lesser extent also facts) have been suffixed with _nat and _int
-respectively. INCOMPATIBILITY.
-
-* Most rules produced by inductive and datatype package have mandatory
-prefixes. INCOMPATIBILITY.
-
* New proof method "smt" for a combination of first-order logic with
equality, linear and nonlinear (natural/integer/real) arithmetic, and
fixed-size bitvectors; there is also basic support for higher-order
@@ -68,6 +55,69 @@
relational model finder. See src/HOL/Tools/Nitpick and
src/HOL/Nitpick_Examples.
+* New testing tool Mirabelle for automated proof tools. Applies
+several tools and tactics like sledgehammer, metis, or quickcheck, to
+every proof step in a theory. To be used in batch mode via the
+"mirabelle" utility.
+
+* New proof method "sos" (sum of squares) for nonlinear real
+arithmetic (originally due to John Harison). It requires theory
+Library/Sum_Of_Squares. It is not a complete decision procedure but
+works well in practice on quantifier-free real arithmetic with +, -,
+*, ^, =, <= and <, i.e. boolean combinations of equalities and
+inequalities between polynomials. It makes use of external
+semidefinite programming solvers. Method "sos" generates a
+certificate that can be pasted into the proof thus avoiding the need
+to call an external tool every time the proof is checked. See
+src/HOL/Library/Sum_Of_Squares.
+
+* New commands 'code_pred' and 'values' to invoke the predicate
+compiler and to enumerate values of inductive predicates.
+
+* A tabled implementation of the reflexive transitive closure.
+
+* New theory SupInf of the supremum and infimum operators for sets of
+reals.
+
+* New theory Probability, which contains a development of measure
+theory, eventually leading to Lebesgue integration and probability.
+
+* New method "linarith" invokes existing linear arithmetic decision
+procedure only.
+
+* New implementation of quickcheck uses generic code generator;
+default generators are provided for all suitable HOL types, records
+and datatypes. Old quickcheck can be re-activated importing theory
+Library/SML_Quickcheck.
+
+* New command 'atp_minimal' reduces result produced by Sledgehammer.
+
+* New Sledgehammer option "Full Types" in Proof General settings menu.
+Causes full type information to be output to the ATPs. This slows
+ATPs down considerably but eliminates a source of unsound "proofs"
+that fail later.
+
+* New method "metisFT": A version of metis that uses full type
+information in order to avoid failures of proof reconstruction.
+
+* New evaluator "approximate" approximates an real valued term using
+the same method as the approximation method.
+
+* Method "approximate" now supports arithmetic expressions as
+boundaries of intervals and implements interval splitting and Taylor
+series expansion.
+
+* ML antiquotation @{code_datatype} inserts definition of a datatype
+generated by the code generator; e.g. see src/HOL/Predicate.thy.
+
+* Combined former theories Divides and IntDiv to one theory Divides in
+the spirit of other number theory theories in HOL; some constants (and
+to a lesser extent also facts) have been suffixed with _nat and _int
+respectively. INCOMPATIBILITY.
+
+* Most rules produced by inductive and datatype package have mandatory
+prefixes. INCOMPATIBILITY.
+
* Reorganization of number theory, INCOMPATIBILITY:
- former session NumberTheory now named Old_Number_Theory
- new session Number_Theory; prefer this, if possible
@@ -85,12 +135,6 @@
* Split off prime number ingredients from theory GCD to theory
Number_Theory/Primes.
-* New theory SupInf of the supremum and infimum operators for sets of
-reals.
-
-* New theory Probability, which contains a development of measure
-theory, eventually leading to Lebesgue integration and probability.
-
* Class semiring_div requires superclass no_zero_divisors and proof of
div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
@@ -111,22 +155,6 @@
* Added theorem List.map_map as [simp]. Removed List.map_compose.
INCOMPATIBILITY.
-* New testing tool "Mirabelle" for automated proof tools. Applies
-several tools and tactics like sledgehammer, metis, or quickcheck, to
-every proof step in a theory. To be used in batch mode via the
-"mirabelle" utility.
-
-* New proof method "sos" (sum of squares) for nonlinear real
-arithmetic (originally due to John Harison). It requires theory
-Library/Sum_Of_Squares. It is not a complete decision procedure but
-works well in practice on quantifier-free real arithmetic with +, -,
-*, ^, =, <= and <, i.e. boolean combinations of equalities and
-inequalities between polynomials. It makes use of external
-semidefinite programming solvers. Method "sos" generates a
-certificate that can be pasted into the proof thus avoiding the need
-to call an external tool every time the proof is checked. See
-src/HOL/Library/Sum_Of_Squares.
-
* Code generator attributes follow the usual underscore convention:
code_unfold replaces code unfold
code_post replaces code post
@@ -197,40 +225,11 @@
abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
INCOMPATIBILITY.
-* ML antiquotation @{code_datatype} inserts definition of a datatype
-generated by the code generator; e.g. see src/HOL/Predicate.thy.
-
-* New method "linarith" invokes existing linear arithmetic decision
-procedure only.
-
-* New implementation of quickcheck uses generic code generator;
-default generators are provided for all suitable HOL types, records
-and datatypes. Old quickcheck can be re-activated importing theory
-Library/SML_Quickcheck.
-
* Renamed theorems:
Suc_eq_add_numeral_1 -> Suc_eq_plus1
Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
Suc_plus1 -> Suc_eq_plus1
-* New sledgehammer option "Full Types" in Proof General settings menu.
-Causes full type information to be output to the ATPs. This slows
-ATPs down considerably but eliminates a source of unsound "proofs"
-that fail later.
-
-* New method "metisFT": A version of metis that uses full type
-information in order to avoid failures of proof reconstruction.
-
-* Discontinued abbreviation "arbitrary" of constant "undefined".
-INCOMPATIBILITY, use "undefined" directly.
-
-* New evaluator "approximate" approximates an real valued term using
-the same method as the approximation method.
-
-* Method "approximate" now supports arithmetic expressions as
-boundaries of intervals and implements interval splitting and Taylor
-series expansion.
-
* Changed "DERIV_intros" to a dynamic fact, which can be augmented by
the attribute of the same name. Each of the theorems in the list
DERIV_intros assumes composition with an additional function and
@@ -248,6 +247,9 @@
* Lemma name change: replaced "anti_sym" by "antisym" everywhere.
INCOMPATIBILITY.
+* Discontinued abbreviation "arbitrary" of constant "undefined".
+INCOMPATIBILITY, use "undefined" directly.
+
*** HOLCF ***
@@ -288,6 +290,13 @@
*** ML ***
+* Support for Poly/ML 5.3.0, with improved reporting of compiler
+errors and run-time exceptions, including detailed source positions.
+
+* Structure Name_Space (formerly NameSpace) now manages uniquely
+identified entries, with some additional information such as source
+position, logical grouping etc.
+
* Theory and context data is now introduced by the simplified and
modernized functors Theory_Data, Proof_Data, Generic_Data. Data needs
to be pure, but the old TheoryDataFun for mutable data (with explicit
@@ -327,6 +336,9 @@
* Renamed several structures FooBar to Foo_Bar. Occasional,
INCOMPATIBILITY.
+* Operations of structure Skip_Proof no longer require quick_and_dirty
+mode, which avoids critical setmp.
+
* Eliminated old Attrib.add_attributes, Method.add_methods and related
combinators for "args". INCOMPATIBILITY, need to use simplified
Attrib/Method.setup introduced in Isabelle2009.
@@ -344,9 +356,6 @@
Syntax.pretty_typ/term directly, preferably with proper context
instead of global theory.
-* Operations of structure Skip_Proof no longer require quick_and_dirty
-mode, which avoids critical setmp.
-
*** System ***