NEWS
changeset 25502 9200b36280c0
parent 25464 0ca80ce89001
child 25508 00b59b9c7c83
equal deleted inserted replaced
25501:845883bd3a6b 25502:9200b36280c0
     1 Isabelle NEWS -- history user-relevant changes
     1 Isabelle NEWS -- history user-relevant changes
     2 ==============================================
     2 ==============================================
     3 
     3 
     4 New in this Isabelle version
     4 New in this Isabelle version
     5 ----------------------------
     5 ----------------------------
       
     6 
       
     7 *** Pure ***
       
     8 
       
     9 * Command "instance" now takes list of definitions in the same
       
    10 manner as the "definition" command.  Most notably, object equality is now
       
    11 possible.  Type inference is more canonical than it used to be.
       
    12 INCOMPATIBILITY: in some cases explicit type annotations are required.
       
    13 
     6 
    14 
     7 *** HOL ***
    15 *** HOL ***
     8 
    16 
     9 * Constant "card" now with authentic syntax.
    17 * Constant "card" now with authentic syntax.
    10 
    18