NEWS
changeset 40821 9f32d7b8b24f
parent 40801 6cfacec435e6
parent 40815 6e2d17cc0d1d
child 40846 5a2ae8cc9d0e
equal deleted inserted replaced
40807:eeaa59fb5ad8 40821:9f32d7b8b24f
    89 * Document antiquotation @{file} checks file/directory entries within
    89 * Document antiquotation @{file} checks file/directory entries within
    90 the local file system.
    90 the local file system.
    91 
    91 
    92 
    92 
    93 *** HOL ***
    93 *** HOL ***
       
    94 
       
    95 * Abandoned locale equiv for equivalence relations.  INCOMPATIBILITY: use
       
    96 equivI rather than equiv_intro.
    94 
    97 
    95 * Code generator: globbing constant expressions "*" and "Theory.*" have been
    98 * Code generator: globbing constant expressions "*" and "Theory.*" have been
    96 replaced by the more idiomatic "_" and "Theory._".  INCOMPATIBILITY.
    99 replaced by the more idiomatic "_" and "Theory._".  INCOMPATIBILITY.
    97 
   100 
    98 * Theory Enum (for explicit enumerations of finite types) is now part of
   101 * Theory Enum (for explicit enumerations of finite types) is now part of