1.1 --- a/NEWS Sun Nov 22 14:13:18 2009 +0100
1.2 +++ b/NEWS Sun Nov 22 14:49:36 2009 +0100
1.3 @@ -12,9 +12,6 @@
1.4
1.5 *** Pure ***
1.6
1.7 -* On instantiation of classes, remaining undefined class parameters
1.8 -are formally declared. INCOMPATIBILITY.
1.9 -
1.10 * Locale interpretation propagates mixins along the locale hierarchy.
1.11 The currently only available mixins are the equations used to map
1.12 local definitions to terms of the target domain of an interpretation.
1.13 @@ -26,6 +23,9 @@
1.14 * Thoroughly revised locales tutorial. New section on conditional
1.15 interpretation.
1.16
1.17 +* On instantiation of classes, remaining undefined class parameters
1.18 +are formally declared. INCOMPATIBILITY.
1.19 +
1.20
1.21 *** Document preparation ***
1.22
1.23 @@ -37,19 +37,6 @@
1.24
1.25 *** HOL ***
1.26
1.27 -* A tabled implementation of the reflexive transitive closure.
1.28 -
1.29 -* New commands 'code_pred' and 'values' to invoke the predicate
1.30 -compiler and to enumerate values of inductive predicates.
1.31 -
1.32 -* Combined former theories Divides and IntDiv to one theory Divides in
1.33 -the spirit of other number theory theories in HOL; some constants (and
1.34 -to a lesser extent also facts) have been suffixed with _nat and _int
1.35 -respectively. INCOMPATIBILITY.
1.36 -
1.37 -* Most rules produced by inductive and datatype package have mandatory
1.38 -prefixes. INCOMPATIBILITY.
1.39 -
1.40 * New proof method "smt" for a combination of first-order logic with
1.41 equality, linear and nonlinear (natural/integer/real) arithmetic, and
1.42 fixed-size bitvectors; there is also basic support for higher-order
1.43 @@ -68,50 +55,7 @@
1.44 relational model finder. See src/HOL/Tools/Nitpick and
1.45 src/HOL/Nitpick_Examples.
1.46
1.47 -* Reorganization of number theory, INCOMPATIBILITY:
1.48 - - former session NumberTheory now named Old_Number_Theory
1.49 - - new session Number_Theory; prefer this, if possible
1.50 - - moved legacy theories Legacy_GCD and Primes from src/HOL/Library
1.51 - to src/HOL/Old_Number_Theory
1.52 - - moved theory Pocklington from src/HOL/Library to
1.53 - src/HOL/Old_Number_Theory
1.54 - - removed various references to Old_Number_Theory from HOL
1.55 - distribution
1.56 -
1.57 -* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
1.58 -of finite and infinite sets. It is shown that they form a complete
1.59 -lattice.
1.60 -
1.61 -* Split off prime number ingredients from theory GCD to theory
1.62 -Number_Theory/Primes.
1.63 -
1.64 -* New theory SupInf of the supremum and infimum operators for sets of
1.65 -reals.
1.66 -
1.67 -* New theory Probability, which contains a development of measure
1.68 -theory, eventually leading to Lebesgue integration and probability.
1.69 -
1.70 -* Class semiring_div requires superclass no_zero_divisors and proof of
1.71 -div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
1.72 -div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
1.73 -generalized to class semiring_div, subsuming former theorems
1.74 -zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
1.75 -zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
1.76 -INCOMPATIBILITY.
1.77 -
1.78 -* Extended Multivariate Analysis to include derivation and Brouwer's
1.79 -fixpoint theorem.
1.80 -
1.81 -* Removed predicate "M hassize n" (<--> card M = n & finite M).
1.82 -INCOMPATIBILITY.
1.83 -
1.84 -* Renamed vector_less_eq_def to vector_le_def, the more usual name.
1.85 -INCOMPATIBILITY.
1.86 -
1.87 -* Added theorem List.map_map as [simp]. Removed List.map_compose.
1.88 -INCOMPATIBILITY.
1.89 -
1.90 -* New testing tool "Mirabelle" for automated proof tools. Applies
1.91 +* New testing tool Mirabelle for automated proof tools. Applies
1.92 several tools and tactics like sledgehammer, metis, or quickcheck, to
1.93 every proof step in a theory. To be used in batch mode via the
1.94 "mirabelle" utility.
1.95 @@ -127,6 +71,90 @@
1.96 to call an external tool every time the proof is checked. See
1.97 src/HOL/Library/Sum_Of_Squares.
1.98
1.99 +* New commands 'code_pred' and 'values' to invoke the predicate
1.100 +compiler and to enumerate values of inductive predicates.
1.101 +
1.102 +* A tabled implementation of the reflexive transitive closure.
1.103 +
1.104 +* New theory SupInf of the supremum and infimum operators for sets of
1.105 +reals.
1.106 +
1.107 +* New theory Probability, which contains a development of measure
1.108 +theory, eventually leading to Lebesgue integration and probability.
1.109 +
1.110 +* New method "linarith" invokes existing linear arithmetic decision
1.111 +procedure only.
1.112 +
1.113 +* New implementation of quickcheck uses generic code generator;
1.114 +default generators are provided for all suitable HOL types, records
1.115 +and datatypes. Old quickcheck can be re-activated importing theory
1.116 +Library/SML_Quickcheck.
1.117 +
1.118 +* New command 'atp_minimal' reduces result produced by Sledgehammer.
1.119 +
1.120 +* New Sledgehammer option "Full Types" in Proof General settings menu.
1.121 +Causes full type information to be output to the ATPs. This slows
1.122 +ATPs down considerably but eliminates a source of unsound "proofs"
1.123 +that fail later.
1.124 +
1.125 +* New method "metisFT": A version of metis that uses full type
1.126 +information in order to avoid failures of proof reconstruction.
1.127 +
1.128 +* New evaluator "approximate" approximates an real valued term using
1.129 +the same method as the approximation method.
1.130 +
1.131 +* Method "approximate" now supports arithmetic expressions as
1.132 +boundaries of intervals and implements interval splitting and Taylor
1.133 +series expansion.
1.134 +
1.135 +* ML antiquotation @{code_datatype} inserts definition of a datatype
1.136 +generated by the code generator; e.g. see src/HOL/Predicate.thy.
1.137 +
1.138 +* Combined former theories Divides and IntDiv to one theory Divides in
1.139 +the spirit of other number theory theories in HOL; some constants (and
1.140 +to a lesser extent also facts) have been suffixed with _nat and _int
1.141 +respectively. INCOMPATIBILITY.
1.142 +
1.143 +* Most rules produced by inductive and datatype package have mandatory
1.144 +prefixes. INCOMPATIBILITY.
1.145 +
1.146 +* Reorganization of number theory, INCOMPATIBILITY:
1.147 + - former session NumberTheory now named Old_Number_Theory
1.148 + - new session Number_Theory; prefer this, if possible
1.149 + - moved legacy theories Legacy_GCD and Primes from src/HOL/Library
1.150 + to src/HOL/Old_Number_Theory
1.151 + - moved theory Pocklington from src/HOL/Library to
1.152 + src/HOL/Old_Number_Theory
1.153 + - removed various references to Old_Number_Theory from HOL
1.154 + distribution
1.155 +
1.156 +* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
1.157 +of finite and infinite sets. It is shown that they form a complete
1.158 +lattice.
1.159 +
1.160 +* Split off prime number ingredients from theory GCD to theory
1.161 +Number_Theory/Primes.
1.162 +
1.163 +* Class semiring_div requires superclass no_zero_divisors and proof of
1.164 +div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
1.165 +div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
1.166 +generalized to class semiring_div, subsuming former theorems
1.167 +zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
1.168 +zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
1.169 +INCOMPATIBILITY.
1.170 +
1.171 +* Extended Multivariate Analysis to include derivation and Brouwer's
1.172 +fixpoint theorem.
1.173 +
1.174 +* Removed predicate "M hassize n" (<--> card M = n & finite M).
1.175 +INCOMPATIBILITY.
1.176 +
1.177 +* Renamed vector_less_eq_def to vector_le_def, the more usual name.
1.178 +INCOMPATIBILITY.
1.179 +
1.180 +* Added theorem List.map_map as [simp]. Removed List.map_compose.
1.181 +INCOMPATIBILITY.
1.182 +
1.183 * Code generator attributes follow the usual underscore convention:
1.184 code_unfold replaces code unfold
1.185 code_post replaces code post
1.186 @@ -197,40 +225,11 @@
1.187 abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
1.188 INCOMPATIBILITY.
1.189
1.190 -* ML antiquotation @{code_datatype} inserts definition of a datatype
1.191 -generated by the code generator; e.g. see src/HOL/Predicate.thy.
1.192 -
1.193 -* New method "linarith" invokes existing linear arithmetic decision
1.194 -procedure only.
1.195 -
1.196 -* New implementation of quickcheck uses generic code generator;
1.197 -default generators are provided for all suitable HOL types, records
1.198 -and datatypes. Old quickcheck can be re-activated importing theory
1.199 -Library/SML_Quickcheck.
1.200 -
1.201 * Renamed theorems:
1.202 Suc_eq_add_numeral_1 -> Suc_eq_plus1
1.203 Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
1.204 Suc_plus1 -> Suc_eq_plus1
1.205
1.206 -* New sledgehammer option "Full Types" in Proof General settings menu.
1.207 -Causes full type information to be output to the ATPs. This slows
1.208 -ATPs down considerably but eliminates a source of unsound "proofs"
1.209 -that fail later.
1.210 -
1.211 -* New method "metisFT": A version of metis that uses full type
1.212 -information in order to avoid failures of proof reconstruction.
1.213 -
1.214 -* Discontinued abbreviation "arbitrary" of constant "undefined".
1.215 -INCOMPATIBILITY, use "undefined" directly.
1.216 -
1.217 -* New evaluator "approximate" approximates an real valued term using
1.218 -the same method as the approximation method.
1.219 -
1.220 -* Method "approximate" now supports arithmetic expressions as
1.221 -boundaries of intervals and implements interval splitting and Taylor
1.222 -series expansion.
1.223 -
1.224 * Changed "DERIV_intros" to a dynamic fact, which can be augmented by
1.225 the attribute of the same name. Each of the theorems in the list
1.226 DERIV_intros assumes composition with an additional function and
1.227 @@ -248,6 +247,9 @@
1.228 * Lemma name change: replaced "anti_sym" by "antisym" everywhere.
1.229 INCOMPATIBILITY.
1.230
1.231 +* Discontinued abbreviation "arbitrary" of constant "undefined".
1.232 +INCOMPATIBILITY, use "undefined" directly.
1.233 +
1.234
1.235 *** HOLCF ***
1.236
1.237 @@ -288,6 +290,13 @@
1.238
1.239 *** ML ***
1.240
1.241 +* Support for Poly/ML 5.3.0, with improved reporting of compiler
1.242 +errors and run-time exceptions, including detailed source positions.
1.243 +
1.244 +* Structure Name_Space (formerly NameSpace) now manages uniquely
1.245 +identified entries, with some additional information such as source
1.246 +position, logical grouping etc.
1.247 +
1.248 * Theory and context data is now introduced by the simplified and
1.249 modernized functors Theory_Data, Proof_Data, Generic_Data. Data needs
1.250 to be pure, but the old TheoryDataFun for mutable data (with explicit
1.251 @@ -327,6 +336,9 @@
1.252 * Renamed several structures FooBar to Foo_Bar. Occasional,
1.253 INCOMPATIBILITY.
1.254
1.255 +* Operations of structure Skip_Proof no longer require quick_and_dirty
1.256 +mode, which avoids critical setmp.
1.257 +
1.258 * Eliminated old Attrib.add_attributes, Method.add_methods and related
1.259 combinators for "args". INCOMPATIBILITY, need to use simplified
1.260 Attrib/Method.setup introduced in Isabelle2009.
1.261 @@ -344,9 +356,6 @@
1.262 Syntax.pretty_typ/term directly, preferably with proper context
1.263 instead of global theory.
1.264
1.265 -* Operations of structure Skip_Proof no longer require quick_and_dirty
1.266 -mode, which avoids critical setmp.
1.267 -
1.268
1.269 *** System ***
1.270