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