NEWS
changeset 71944 18357df1cd20
parent 71941 49af3d9a818c
child 71945 4b1264316270
equal deleted inserted replaced
71943:d3fb19847662 71944:18357df1cd20
    48 
    48 
    49 * For the natural numbers, Sup {} = 0.
    49 * For the natural numbers, Sup {} = 0.
    50 
    50 
    51 * Session HOL-Word: Operation "bin_last" is now a mere input
    51 * Session HOL-Word: Operation "bin_last" is now a mere input
    52 abbreviation.  Minor INCOMPATIBILITY.
    52 abbreviation.  Minor INCOMPATIBILITY.
       
    53 
       
    54 * Session HOL-Word: Compound operation "bin_split" simplifies by default
       
    55 into its components "drop_bit" and "take_bit".  Minor INCOMPATIBILITY.
    53 
    56 
    54 
    57 
    55 *** FOL ***
    58 *** FOL ***
    56 
    59 
    57 * Added the "at most 1" quantifier, Uniq, as in HOL.
    60 * Added the "at most 1" quantifier, Uniq, as in HOL.