NEWS
changeset 34962 807f6ce0273d
parent 34946 aa5d27f1d9b9
child 34974 18b41bba42b5
child 36093 0880493627ca
equal deleted inserted replaced
34947:e1b8f2736404 34962:807f6ce0273d
     9 * Code generator: details of internal data cache have no impact on
     9 * Code generator: details of internal data cache have no impact on
    10 the user space functionality any longer.
    10 the user space functionality any longer.
    11 
    11 
    12 
    12 
    13 *** HOL ***
    13 *** HOL ***
       
    14 
       
    15 * HOLogic.strip_psplit: types are returned in syntactic order, similar
       
    16 to other strip and tuple operations.  INCOMPATIBILITY.
    14 
    17 
    15 * Various old-style primrec specifications in the HOL theories have been
    18 * Various old-style primrec specifications in the HOL theories have been
    16 replaced by new-style primrec, especially in theory List.  The corresponding
    19 replaced by new-style primrec, especially in theory List.  The corresponding
    17 constants now have authentic syntax.  INCOMPATIBILITY.
    20 constants now have authentic syntax.  INCOMPATIBILITY.
    18 
    21