NEWS
changeset 68100 b2d84b1114fa
parent 68080 17f79ae49401
child 68116 ac82ee617a75
     1.1 --- a/NEWS	Sun May 06 18:20:25 2018 +0000
     1.2 +++ b/NEWS	Sun May 06 18:20:25 2018 +0000
     1.3 @@ -278,10 +278,6 @@
     1.4  HOL-Computational_Algebra.Field_as_Ring explicitly in case of need.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 -* Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid
     1.8 -clash with fact mod_mult_self4 (on more generic semirings).
     1.9 -INCOMPATIBILITY.
    1.10 -
    1.11  * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to
    1.12  sum.swap(_restrict) and prod.swap(_restrict), to avoid name clashes on
    1.13  interpretation of abstract locales. INCOMPATIBILITY.
    1.14 @@ -318,6 +314,18 @@
    1.15  * Code generation: Code generation takes an explicit option
    1.16  "case_insensitive" to accomodate case-insensitive file systems.
    1.17  
    1.18 +* Fact mod_mult_self4 (on nat) renamed to Suc_mod_mult_self3, to avoid
    1.19 +clash with fact mod_mult_self4 (on more generic semirings).
    1.20 +INCOMPATIBILITY.
    1.21 +
    1.22 +* Eliminated some theorem aliasses:
    1.23 +
    1.24 +  even_times_iff ~> even_mult_iff
    1.25 +  mod_2_not_eq_zero_eq_one_nat ~> not_mod_2_eq_0_eq_1
    1.26 +  even_of_nat ~> even_int_iff
    1.27 +
    1.28 +INCOMPATIBILITY.
    1.29 +
    1.30  
    1.31  *** System ***
    1.32