NEWS
changeset 55818 d8b2f50705d0
parent 55757 9fc71814b8c1
child 55867 79b915f26533
equal deleted inserted replaced
55817:0bc0217387a5 55818:d8b2f50705d0
    88 (only makes sense in practice, if outer syntax is delimited
    88 (only makes sense in practice, if outer syntax is delimited
    89 differently).
    89 differently).
    90 
    90 
    91 
    91 
    92 *** HOL ***
    92 *** HOL ***
       
    93 
       
    94 * HOL-Word:
       
    95   * Abandoned fact collection "word_arith_alts", which is a
       
    96   duplicate of "word_arith_wis".
       
    97   * Dropped first (duplicated) element in fact collections
       
    98   "sint_word_ariths", "word_arith_alts", "uint_word_ariths",
       
    99   "uint_word_arith_bintrs".
    93 
   100 
    94 * Code generator: explicit proof contexts in many ML interfaces.
   101 * Code generator: explicit proof contexts in many ML interfaces.
    95 INCOMPATIBILITY.
   102 INCOMPATIBILITY.
    96 
   103 
    97 * Code generator: minimize exported identifiers by default.
   104 * Code generator: minimize exported identifiers by default.