NEWS
changeset 52148 893b15200ec1
parent 52141 eff000cab70f
parent 52143 36ffe23b25f8
child 52266 86d6f57c2c1e
equal deleted inserted replaced
52141:eff000cab70f 52148:893b15200ec1
    37 
    37 
    38 * Option to skip over proofs, using implicit 'sorry' internally.
    38 * Option to skip over proofs, using implicit 'sorry' internally.
    39 
    39 
    40 
    40 
    41 *** Pure ***
    41 *** Pure ***
       
    42 
       
    43 * Syntax translation functions (print_translation etc.) always depend
       
    44 on Proof.context.  Discontinued former "(advanced)" option -- this is
       
    45 now the default.  Minor INCOMPATIBILITY.
    42 
    46 
    43 * Target-sensitive commands 'interpretation' and 'sublocale'.
    47 * Target-sensitive commands 'interpretation' and 'sublocale'.
    44 Particulary, 'interpretation' now allows for non-persistent
    48 Particulary, 'interpretation' now allows for non-persistent
    45 interpretation within "context ... begin ... end" blocks.
    49 interpretation within "context ... begin ... end" blocks.
    46 See "isar-ref" manual for details.
    50 See "isar-ref" manual for details.