NEWS
changeset 65170 53675f36820d
parent 65099 30d0b2f1df76
child 65329 4f3da52cec02
equal deleted inserted replaced
65169:a8dfa258bf93 65170:53675f36820d
    45 the document model to theories that are required for open editor
    45 the document model to theories that are required for open editor
    46 buffers.
    46 buffers.
    47 
    47 
    48 
    48 
    49 *** HOL ***
    49 *** HOL ***
       
    50 
       
    51 * Constant "surj" is a full input/output abbreviation (again).
       
    52 Minor INCOMPATIBILITY.
    50 
    53 
    51 * Theory Library/FinFun has been moved to AFP (again).  INCOMPATIBILITY.
    54 * Theory Library/FinFun has been moved to AFP (again).  INCOMPATIBILITY.
    52 
    55 
    53 * Some old and rarely used ASCII replacement syntax has been removed.
    56 * Some old and rarely used ASCII replacement syntax has been removed.
    54 INCOMPATIBILITY, standard syntax with symbols should be used instead.
    57 INCOMPATIBILITY, standard syntax with symbols should be used instead.