NEWS
changeset 64593 50c715579715
parent 64555 628b271c5b8b
child 64602 8edca3465758
     1.1 --- a/NEWS	Sat Dec 17 15:22:14 2016 +0100
     1.2 +++ b/NEWS	Sat Dec 17 15:22:14 2016 +0100
     1.3 @@ -6,6 +6,24 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Swapped orientation of congruence rules mod_add_left_eq,
    1.10 +mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
    1.11 +mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
    1.12 +mod_diff_eq.  INCOMPATIBILITY.
    1.13 +
    1.14 +* Generalized some facts:
    1.15 +    zminus_zmod ~> mod_minus_eq
    1.16 +    zdiff_zmod_left ~> mod_diff_left_eq
    1.17 +    zdiff_zmod_right ~> mod_diff_right_eq
    1.18 +    zmod_eq_dvd_iff ~> mod_eq_dvd_iff
    1.19 +INCOMPATIBILITY.
    1.20 +
    1.21 +* Named collection mod_simps covers various congruence rules
    1.22 +concerning mod, replacing former zmod_simps.
    1.23 +INCOMPATIBILITY.
    1.24 +
    1.25  * (Co)datatype package:
    1.26    - The 'size_gen_o_map' lemma is no longer generated for datatypes
    1.27      with type class annotations. As a result, the tactic that derives
    1.28 @@ -74,7 +92,6 @@
    1.29  * Solve direct: option "solve_direct_strict_warnings" gives explicit
    1.30  warnings for lemma statements with trivial proofs.
    1.31  
    1.32 -
    1.33  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.34  
    1.35  * More aggressive flushing of machine-generated input, according to