--- a/NEWS Thu Sep 17 19:13:22 2009 +0200
+++ b/NEWS Fri Sep 18 07:54:26 2009 +0200
@@ -19,14 +19,28 @@
*** HOL ***
* Reorganization of number theory:
- * former session NumberTheory now named Old_Number_Theory; former session NewNumberTheory
- named NumberTheory;
- * split off prime number ingredients from theory GCD to theory Number_Theory/Primes;
+ * former session NumberTheory now named Old_Number_Theory
+ * new session Number_Theory by Jeremy Avigad; if possible, prefer this.
* moved legacy theories Legacy_GCD and Primes from Library/ to Old_Number_Theory/;
* moved theory Pocklington from Library/ to Old_Number_Theory/;
* removed various references to Old_Number_Theory from HOL distribution.
INCOMPATIBILITY.
+* Theory GCD now has 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.
+
+* Split off prime number ingredients from theory GCD
+to theory Number_Theory/Primes;
+
+* 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
+generalized to class semiring_div, subsuming former theorems
+zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
+zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
+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
@@ -47,16 +61,15 @@
etc.
INCOMPATIBILITY.
-* New class "boolean_algebra".
-
* Refinements to lattice classes and sets:
- less default intro/elim rules in locale variant, more default
intro/elim rules in class variant: more uniformity
- lemma ge_sup_conv renamed to le_sup_iff, in accordance with le_inf_iff
- dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and sup_aci)
- renamed ACI to inf_sup_aci
+ - new class "boolean_algebra"
- class "complete_lattice" moved to separate theory "complete_lattice";
- corresponding constants (and abbreviations) renamed:
+ corresponding constants (and abbreviations) renamed and with authentic syntax:
Set.Inf ~> Complete_Lattice.Inf
Set.Sup ~> Complete_Lattice.Sup
Set.INFI ~> Complete_Lattice.INFI
@@ -68,22 +81,18 @@
- more convenient names for set intersection and union:
Set.Int ~> Set.inter
Set.Un ~> Set.union
+ - authentic syntax for
+ Set.Pow
+ Set.image
- mere abbreviations:
Set.empty (for bot)
Set.UNIV (for top)
Complete_Lattice.Inter (for Inf)
Complete_Lattice.Union (for Sup)
+ - object-logic definitions as far as appropriate
INCOMPATIBILITY.
-* 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
-generalized to class semiring_div, subsuming former theorems
-zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
-zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
-INCOMPATIBILITY.
-
* Power operations on relations and functions are now one dedicate
constant "compow" with infix syntax "^^". Power operations on
multiplicative monoids retains syntax "^" and is now defined generic
@@ -96,10 +105,6 @@
this. Fix using O_assoc[symmetric]. The same applies to the curried
version "R OO S".
-* Theory GCD now has 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.
-
* ML antiquotation @{code_datatype} inserts definition of a datatype
generated by the code generator; see Predicate.thy for an example.
@@ -110,10 +115,6 @@
default generators are provided for all suitable HOL types, records
and datatypes.
-* Constants Set.Pow and Set.image now with authentic syntax;
-object-logic definitions Set.Pow_def and Set.image_def.
-INCOMPATIBILITY.
-
* Renamed theorems:
Suc_eq_add_numeral_1 -> Suc_eq_plus1
Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
@@ -138,9 +139,6 @@
INCOMPATIBILITY.
-* NewNumberTheory: Jeremy Avigad's new version of part of
-NumberTheory. If possible, use NewNumberTheory, not NumberTheory.
-
* Discontinued abbreviation "arbitrary" of constant
"undefined". INCOMPATIBILITY, use "undefined" directly.