NEWS
changeset 44274 731b18266d5a
parent 44136 e63ad7d5158d
child 44282 f0de18b62d63
equal deleted inserted replaced
44263:971d1be5d5ce 44274:731b18266d5a
    54 that the result needs to be unique, which means fact specifications
    54 that the result needs to be unique, which means fact specifications
    55 may have to be refined after enriching a proof context.
    55 may have to be refined after enriching a proof context.
    56 
    56 
    57 * Isabelle/Isar reference manual provides more formal references in
    57 * Isabelle/Isar reference manual provides more formal references in
    58 syntax diagrams.
    58 syntax diagrams.
       
    59 
       
    60 * Attribute case_names has been refined: the assumptions in each case can
       
    61 be named now by following the case name with [name1 name2 ...].
    59 
    62 
    60 
    63 
    61 *** HOL ***
    64 *** HOL ***
    62 
    65 
    63 * Classes bot and top require underlying partial order rather than preorder:
    66 * Classes bot and top require underlying partial order rather than preorder: