updated NEWS and CONTRIBUTORS
authorblanchet
Tue Aug 28 17:17:25 2012 +0200 (2012-08-28)
changeset 48977ae12b92c145a
parent 48976 2d17c305f4bc
child 48978 dcb486124b6a
updated NEWS and CONTRIBUTORS
CONTRIBUTORS
NEWS
     1.1 --- a/CONTRIBUTORS	Tue Aug 28 17:17:03 2012 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Aug 28 17:17:25 2012 +0200
     1.3 @@ -6,6 +6,12 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM
     1.8 +  New (co)datatype package.
     1.9 +
    1.10 +* August 2012: Andrei Popescu and Dmitriy Traytel, TUM
    1.11 +  Theories of ordinals and cardinals.
    1.12 +
    1.13  * July 2012: Makarius Wenzel, Université Paris-Sud / LRI
    1.14    Advanced support for Isabelle sessions and build management, notably
    1.15    "isabelle build".
    1.16 @@ -161,7 +167,7 @@
    1.17  * November 2009: Lukas Bulwahn, TUM
    1.18    Predicate Compiler: a compiler for inductive predicates to
    1.19    equational specifications.
    1.20 - 
    1.21 +
    1.22  * November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris
    1.23    HOL-Boogie: an interactive prover back-end for Boogie and VCC.
    1.24  
     2.1 --- a/NEWS	Tue Aug 28 17:17:03 2012 +0200
     2.2 +++ b/NEWS	Tue Aug 28 17:17:25 2012 +0200
     2.3 @@ -41,6 +41,12 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* HOL/Codatatype: New (co)datatype package with support for mixed,
     2.8 +nested recursion and interesting non-free datatypes.
     2.9 +
    2.10 +* HOL/Ordinals_and_Cardinals: Theories of ordinals and cardinals
    2.11 +(supersedes the AFP entry of the same name).
    2.12 +
    2.13  * Library/Debug.thy and Library/Parallel.thy: debugging and parallel
    2.14  execution for code generated towards Isabelle/ML.
    2.15  
    2.16 @@ -51,7 +57,7 @@
    2.17  
    2.18    - added an optimisation for equality premises.
    2.19      It is switched on by default, and can be switched off by setting
    2.20 -    the configuration quickcheck_optimise_equality to false.    
    2.21 +    the configuration quickcheck_optimise_equality to false.
    2.22  
    2.23  * The SMT solver Z3 has now by default a restricted set of directly
    2.24  supported features. For the full set of features (div/mod, nonlinear
    2.25 @@ -4557,7 +4563,7 @@
    2.26  type and generates all solutions by prolog-style backwards proof using
    2.27  the declared rules.
    2.28  
    2.29 -This setup also deals with rules like 
    2.30 +This setup also deals with rules like
    2.31  
    2.32    "is_measure f ==> is_measure (list_size f)"
    2.33  
    2.34 @@ -5329,7 +5335,7 @@
    2.35  rewrites now. That is, trace_simp_depth_limit is set to 1 by
    2.36  default. Thus there is less danger of being flooded by the trace. The
    2.37  trace indicates where parts have been suppressed.
    2.38 -  
    2.39 +
    2.40  * Provers/classical: removed obsolete classical version of elim_format
    2.41  attribute; classical elim/dest rules are now treated uniformly when
    2.42  manipulating the claset.
    2.43 @@ -5368,7 +5374,7 @@
    2.44  Examples are in the directory MetisExamples.  WARNING: the
    2.45  Isabelle/HOL-Metis integration does not yet work properly with
    2.46  multi-threading.
    2.47 -  
    2.48 +
    2.49  * Command 'sledgehammer' invokes external automatic theorem provers as
    2.50  background processes.  It generates calls to the "metis" method if
    2.51  successful. These can be pasted into the proof.  Users do not have to
    2.52 @@ -5734,7 +5740,7 @@
    2.53  users are encouraged to use the new package.
    2.54  
    2.55  * Method "lexicographic_order" automatically synthesizes termination
    2.56 -relations as lexicographic combinations of size measures. 
    2.57 +relations as lexicographic combinations of size measures.
    2.58  
    2.59  * Case-expressions allow arbitrary constructor-patterns (including
    2.60  "_") and take their order into account, like in functional
    2.61 @@ -5818,7 +5824,7 @@
    2.62  (K x) r The K-combinator that is internally used is called K_record.
    2.63  INCOMPATIBILITY: Usage of the plain update functions has to be
    2.64  adapted.
    2.65 - 
    2.66 +
    2.67  * Class "semiring_0" now contains annihilation axioms x * 0 = 0 and 0
    2.68  * x = 0, which are required for a semiring.  Richer structures do not
    2.69  inherit from semiring_0 anymore, because this property is a theorem
    2.70 @@ -6714,19 +6720,19 @@
    2.71    mult_neg_le        now named mult_nonpos_nonpos
    2.72  
    2.73  * The following lemmas in Ring_and_Field have been added to the simplifier:
    2.74 -     
    2.75 +
    2.76       zero_le_square
    2.77 -     not_square_less_zero 
    2.78 +     not_square_less_zero
    2.79  
    2.80    The following lemmas have been deleted from Real/RealPow:
    2.81 -  
    2.82 +
    2.83       realpow_zero_zero
    2.84       realpow_two
    2.85       realpow_less
    2.86       zero_le_power
    2.87       realpow_two_le
    2.88       abs_realpow_two
    2.89 -     realpow_two_abs     
    2.90 +     realpow_two_abs
    2.91  
    2.92  * Theory Parity: added rules for simplifying exponents.
    2.93