NEWS
changeset 35765 09e238561460
parent 35763 765f8adf10f9
child 35810 a50237ec0ecd
equal deleted inserted replaced
35764:f7f88f2e004f 35765:09e238561460
    61 * Use of cumulative prems via "!" in some proof methods has been
    61 * Use of cumulative prems via "!" in some proof methods has been
    62 discontinued (legacy feature).
    62 discontinued (legacy feature).
    63 
    63 
    64 
    64 
    65 *** Pure ***
    65 *** Pure ***
       
    66 
       
    67 * Local theory specifications may depend on extra type variables that
       
    68 are not present in the result type -- arguments TYPE('a) :: 'a itself
       
    69 are added internally.  For example:
       
    70 
       
    71   definition unitary :: bool where "unitary = (ALL (x::'a) y. x = y)"
    66 
    72 
    67 * Code generator: details of internal data cache have no impact on
    73 * Code generator: details of internal data cache have no impact on
    68 the user space functionality any longer.
    74 the user space functionality any longer.
    69 
    75 
    70 * Discontinued unnamed infix syntax (legacy feature for many years) --
    76 * Discontinued unnamed infix syntax (legacy feature for many years) --