NEWS

 Compiler (VCC) or Spec#).  See src/HOL/Boogie.
 
 * New counterexample generator tool 'nitpick' based on the Kodkod
 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
 "mirabelle" utility.

 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

 series expansion.
 
 * 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
     theories Divides and GCD as well as in new session
     Number_Theory

     including theories Legacy_GCD and Primes (prefer Number_Theory
     if possible)
   - 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.
 
 * 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.
-
-* 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
   - lemma ge_sup_conv renamed to le_sup_iff, in accordance with

   - 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)
+    "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)
     Complete_Lattice.UNION  (for SUPR)
   - object-logic definitions as far as appropriate

 
 * Function "Inv" is renamed to "inv_into" and function "inv" is now an
 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 ***
 
 * Theory Representable defines a class "rep" of domains that are