NEWS
changeset 63113 fe31996e3898
parent 63094 056ea294c256
child 63116 32492105b015
child 63117 acb6d72fc42e
child 63120 629a4c5e953e
equal deleted inserted replaced
63112:6813818baa67 63113:fe31996e3898
   114   - Renamed lemmas:
   114   - Renamed lemmas:
   115       rel_prod_apply ~> rel_prod_inject
   115       rel_prod_apply ~> rel_prod_inject
   116       pred_prod_apply ~> pred_prod_inject
   116       pred_prod_apply ~> pred_prod_inject
   117     INCOMPATIBILITY.
   117     INCOMPATIBILITY.
   118   - The "size" plugin has been made compatible again with locales.
   118   - The "size" plugin has been made compatible again with locales.
       
   119 
       
   120 * Removed obsolete theorem nat_less_cases. INCOMPATIBILITY, use
       
   121 linorder_cases instead.
   119 
   122 
   120 * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
   123 * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
   121 resemble the f.split naming convention, INCOMPATIBILITY.
   124 resemble the f.split naming convention, INCOMPATIBILITY.
   122 
   125 
   123 * Characters (type char) are modelled as finite algebraic type
   126 * Characters (type char) are modelled as finite algebraic type