NEWS
authorpaulson <lp15@cam.ac.uk>
Fri Jun 13 14:49:59 2014 +0100 (2014-06-13)
changeset 572536515cf25de13
parent 57252 19b7ace1c5da
child 57254 d3d91422f408
NEWS
NEWS
     1.1 --- a/NEWS	Fri Jun 13 14:08:20 2014 +0200
     1.2 +++ b/NEWS	Fri Jun 13 14:49:59 2014 +0100
     1.3 @@ -479,7 +479,7 @@
     1.4  
     1.5  For min_ac or max_ac, prefer more general collection ac_simps.
     1.6  
     1.7 -INCOMPATBILITY. 
     1.8 +INCOMPATBILITY.
     1.9  
    1.10  * Word library: bit representations prefer type bool over type bit.
    1.11  INCOMPATIBILITY.
    1.12 @@ -675,6 +675,8 @@
    1.13  
    1.14  * HOL-Multivariate_Analysis:
    1.15    - type class ordered_real_vector for ordered vector spaces
    1.16 +  - new theory Complex_Basic_Analysis defining complex derivatives,
    1.17 +    holomorphic functions, etc., ported from HOL Light's canal.ml.
    1.18    - changed order of ordered_euclidean_space to be compatible with
    1.19      pointwise ordering on products. Therefore instance of
    1.20      conditionally_complete_lattice and ordered_real_vector.
    1.21 @@ -6308,7 +6310,7 @@
    1.22  type and generates all solutions by Prolog-style backward proof using
    1.23  the declared rules.
    1.24  
    1.25 -This setup also deals with rules like 
    1.26 +This setup also deals with rules like
    1.27  
    1.28    "is_measure f ==> is_measure (list_size f)"
    1.29  
    1.30 @@ -7080,7 +7082,7 @@
    1.31  rewrites now. That is, trace_simp_depth_limit is set to 1 by
    1.32  default. Thus there is less danger of being flooded by the trace. The
    1.33  trace indicates where parts have been suppressed.
    1.34 -  
    1.35 +
    1.36  * Provers/classical: removed obsolete classical version of elim_format
    1.37  attribute; classical elim/dest rules are now treated uniformly when
    1.38  manipulating the claset.
    1.39 @@ -7119,7 +7121,7 @@
    1.40  Examples are in the directory MetisExamples.  WARNING: the
    1.41  Isabelle/HOL-Metis integration does not yet work properly with
    1.42  multi-threading.
    1.43 -  
    1.44 +
    1.45  * Command 'sledgehammer' invokes external automatic theorem provers as
    1.46  background processes.  It generates calls to the "metis" method if
    1.47  successful. These can be pasted into the proof.  Users do not have to
    1.48 @@ -7485,7 +7487,7 @@
    1.49  users are encouraged to use the new package.
    1.50  
    1.51  * Method "lexicographic_order" automatically synthesizes termination
    1.52 -relations as lexicographic combinations of size measures. 
    1.53 +relations as lexicographic combinations of size measures.
    1.54  
    1.55  * Case-expressions allow arbitrary constructor-patterns (including
    1.56  "_") and take their order into account, like in functional
    1.57 @@ -7569,7 +7571,7 @@
    1.58  (K x) r The K-combinator that is internally used is called K_record.
    1.59  INCOMPATIBILITY: Usage of the plain update functions has to be
    1.60  adapted.
    1.61 - 
    1.62 +
    1.63  * Class "semiring_0" now contains annihilation axioms x * 0 = 0 and 0
    1.64  * x = 0, which are required for a semiring.  Richer structures do not
    1.65  inherit from semiring_0 anymore, because this property is a theorem
    1.66 @@ -8465,19 +8467,19 @@
    1.67    mult_neg_le        now named mult_nonpos_nonpos
    1.68  
    1.69  * The following lemmas in Ring_and_Field have been added to the simplifier:
    1.70 -     
    1.71 +
    1.72       zero_le_square
    1.73 -     not_square_less_zero 
    1.74 +     not_square_less_zero
    1.75  
    1.76    The following lemmas have been deleted from Real/RealPow:
    1.77 -  
    1.78 +
    1.79       realpow_zero_zero
    1.80       realpow_two
    1.81       realpow_less
    1.82       zero_le_power
    1.83       realpow_two_le
    1.84       abs_realpow_two
    1.85 -     realpow_two_abs     
    1.86 +     realpow_two_abs
    1.87  
    1.88  * Theory Parity: added rules for simplifying exponents.
    1.89