NEWS
changeset 35372 ca158c7b1144
parent 35306 d28f453bf622
child 35377 d84eec579695
equal deleted inserted replaced
35371:6c92eb394e3c 35372:ca158c7b1144
    49 datatype constructors have been renamed from InfixName to Infix etc.
    49 datatype constructors have been renamed from InfixName to Infix etc.
    50 Minor INCOMPATIBILITY.
    50 Minor INCOMPATIBILITY.
    51 
    51 
    52 
    52 
    53 *** HOL ***
    53 *** HOL ***
       
    54 
       
    55 * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc.
       
    56 INCOMPATIBILITY.
    54 
    57 
    55 * New set of rules "ac_simps" provides combined assoc / commute rewrites
    58 * New set of rules "ac_simps" provides combined assoc / commute rewrites
    56 for all interpretations of the appropriate generic locales.
    59 for all interpretations of the appropriate generic locales.
    57 
    60 
    58 * Renamed theory "OrderedGroup" to "Groups" and split theory "Ring_and_Field"
    61 * Renamed theory "OrderedGroup" to "Groups" and split theory "Ring_and_Field"