NEWS
changeset 71946 4d4079159be7
parent 71945 4b1264316270
child 71947 476b9e6904d9
equal deleted inserted replaced
71945:4b1264316270 71946:4d4079159be7
    46 
    46 
    47 * Added the "at most 1" quantifier, Uniq.
    47 * Added the "at most 1" quantifier, Uniq.
    48 
    48 
    49 * For the natural numbers, Sup {} = 0.
    49 * For the natural numbers, Sup {} = 0.
    50 
    50 
    51 * Session HOL-Word: Operations "bin_last" and "bin_rest" are now mere
    51 * Session HOL-Word: Operations "bin_last", "bin_rest" and "max_word"
    52 input abbreviations.  INCOMPATIBILITY.
    52 are now mere input abbreviations.  INCOMPATIBILITY.
    53 
    53 
    54 * Session HOL-Word: Compound operation "bin_split" simplifies by default
    54 * Session HOL-Word: Compound operation "bin_split" simplifies by default
    55 into its components "drop_bit" and "take_bit".  Minor INCOMPATIBILITY.
    55 into its components "drop_bit" and "take_bit".  Minor INCOMPATIBILITY.
    56 
    56 
    57 
    57