# HG changeset patch # User wenzelm # Date 1258897776 -3600 # Node ID 23d09560d56df319138ea14bf755faacad405f4e # Parent efa1b89c79e09da80ae98bb4e2f45c0584395148 more NEWS, more tuning for release; diff -r efa1b89c79e0 -r 23d09560d56d CONTRIBUTORS --- 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 diff -r efa1b89c79e0 -r 23d09560d56d NEWS --- 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 ***