NEWS
changeset 64240 eabf80376aab
parent 64122 74fde524799e
child 64242 93c6f0da5c70
     1.1 --- a/NEWS	Sun Oct 16 09:31:03 2016 +0200
     1.2 +++ b/NEWS	Sun Oct 16 09:31:04 2016 +0200
     1.3 @@ -249,6 +249,21 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Sligthly more standardized theorem names:
     1.8 +    sgn_times ~> sgn_mult
     1.9 +    sgn_mult' ~> Real_Vector_Spaces.sgn_mult
    1.10 +    divide_zero_left ~> div_0
    1.11 +    zero_mod_left ~> mod_0
    1.12 +    divide_zero ~> div_by_0
    1.13 +    divide_1 ~> div_by_1
    1.14 +    nonzero_mult_divide_cancel_left ~> nonzero_mult_div_cancel_left
    1.15 +    div_mult_self1_is_id ~> nonzero_mult_div_cancel_left
    1.16 +    nonzero_mult_divide_cancel_right ~> nonzero_mult_div_cancel_right
    1.17 +    div_mult_self2_is_id ~> nonzero_mult_div_cancel_right
    1.18 +    is_unit_divide_mult_cancel_left ~> is_unit_div_mult_cancel_left
    1.19 +    is_unit_divide_mult_cancel_right ~> is_unit_div_mult_cancel_right
    1.20 +INCOMPATIBILITY.
    1.21 +
    1.22  * Dedicated syntax LENGTH('a) for length of types.
    1.23  
    1.24  * New proof method "argo" using the built-in Argo solver based on SMT