--- a/NEWS Sun Nov 22 22:10:31 2009 +0100
+++ b/NEWS Mon Nov 23 16:15:18 2009 +0100
@@ -55,6 +55,16 @@
relational model finder. See src/HOL/Tools/Nitpick and
src/HOL/Nitpick_Examples.
+* 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 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 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
@@ -71,25 +81,9 @@
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.
@@ -110,8 +104,14 @@
* ML antiquotation @{code_datatype} inserts definition of a datatype
generated by the code generator; e.g. see src/HOL/Predicate.thy.
-* Most rules produced by inductive and datatype package have mandatory
-prefixes. INCOMPATIBILITY.
+* 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.
+
+* Extended Multivariate Analysis to include derivation and Brouwer's
+fixpoint theorem.
* Reorganization of number theory, INCOMPATIBILITY:
- new number theory development for nat and int, in
@@ -125,7 +125,7 @@
- moved theory Pocklington from src/HOL/Library to
src/HOL/Old_Number_Theory
-* Theory GCD now has functions Gcd/GCD and Lcm/LCM for the gcd and lcm
+* Theory GCD includes functions Gcd/GCD and Lcm/LCM for the gcd and lcm
of finite and infinite sets. It is shown that they form a complete
lattice.
@@ -137,24 +137,6 @@
zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
INCOMPATIBILITY.
-* Extended Multivariate Analysis to include derivation and Brouwer's
-fixpoint theorem.
-
-* Removed predicate "M hassize n" (<--> card M = n & finite M).
-INCOMPATIBILITY.
-
-* Renamed vector_less_eq_def to vector_le_def, the more usual name.
-INCOMPATIBILITY.
-
-* Added theorem List.map_map as [simp]. Removed List.map_compose.
-INCOMPATIBILITY.
-
-* Code generator attributes follow the usual underscore convention:
- code_unfold replaces code unfold
- code_post replaces code post
- etc.
- INCOMPATIBILITY.
-
* Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
@@ -165,27 +147,24 @@
- renamed ACI to inf_sup_aci
- new class "boolean_algebra"
- class "complete_lattice" moved to separate theory
- "complete_lattice"; corresponding constants (and abbreviations)
+ "Complete_Lattice"; corresponding constants (and abbreviations)
renamed and with authentic syntax:
- Set.Inf ~> Complete_Lattice.Inf
- Set.Sup ~> Complete_Lattice.Sup
- Set.INFI ~> Complete_Lattice.INFI
- Set.SUPR ~> Complete_Lattice.SUPR
- Set.Inter ~> Complete_Lattice.Inter
- Set.Union ~> Complete_Lattice.Union
- Set.INTER ~> Complete_Lattice.INTER
- Set.UNION ~> Complete_Lattice.UNION
- - more convenient names for set intersection and union:
- Set.Int ~> Set.inter
- Set.Un ~> Set.union
+ Set.Inf ~> Complete_Lattice.Inf
+ Set.Sup ~> Complete_Lattice.Sup
+ Set.INFI ~> Complete_Lattice.INFI
+ Set.SUPR ~> Complete_Lattice.SUPR
+ Set.Inter ~> Complete_Lattice.Inter
+ Set.Union ~> Complete_Lattice.Union
+ Set.INTER ~> Complete_Lattice.INTER
+ Set.UNION ~> Complete_Lattice.UNION
- authentic syntax for
Set.Pow
Set.image
- mere abbreviations:
Set.empty (for bot)
Set.UNIV (for top)
- Set.inter (for inf)
- Set.union (for sup)
+ Set.inter (for inf, formerly Set.Int)
+ Set.union (for sup, formerly Set.Un)
Complete_Lattice.Inter (for Inf)
Complete_Lattice.Union (for Sup)
Complete_Lattice.INTER (for INFI)
@@ -219,31 +198,47 @@
abbreviation for "inv_into UNIV". Lemmas are renamed accordingly.
INCOMPATIBILITY.
-* 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
+--
+
+* Most rules produced by inductive and datatype package have mandatory
+prefixes. INCOMPATIBILITY.
* 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
matches a variable to the derivative, which has to be solved by the
Simplifier. Hence (auto intro!: DERIV_intros) computes the derivative
-of most elementary terms.
-
-* Former Maclauren.DERIV_tac and Maclauren.deriv_tac are superseded
-are replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
+of most elementary terms. Former Maclauren.DERIV_tac and Maclauren.deriv_tac
+should be replaced by (auto intro!: DERIV_intros). INCOMPATIBILITY.
+
+* Code generator attributes follow the usual underscore convention:
+ code_unfold replaces code unfold
+ code_post replaces code post
+ etc.
+ INCOMPATIBILITY.
* Renamed methods:
sizechange -> size_change
induct_scheme -> induction_schema
-
-* Lemma name change: replaced "anti_sym" by "antisym" everywhere.
-INCOMPATIBILITY.
+ INCOMPATIBILITY.
* Discontinued abbreviation "arbitrary" of constant "undefined".
INCOMPATIBILITY, use "undefined" directly.
+* 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
+ *anti_sym -> *antisym*
+ vector_less_eq_def -> vector_le_def
+ INCOMPATIBILITY.
+
+* Added theorem List.map_map as [simp]. Removed List.map_compose.
+INCOMPATIBILITY.
+
+* Removed predicate "M hassize n" (<--> card M = n & finite M).
+INCOMPATIBILITY.
+
*** HOLCF ***