NEWS
changeset 45614 e19788cb0a1a
parent 45600 1bbbac9a0cb0
child 45620 f2a587696afb
equal deleted inserted replaced
45613:70e5b43535cd 45614:e19788cb0a1a
     3 
     3 
     4 New in this Isabelle version
     4 New in this Isabelle version
     5 ----------------------------
     5 ----------------------------
     6 
     6 
     7 *** General ***
     7 *** General ***
       
     8 
       
     9 * Prover IDE (PIDE) improvements:
       
    10 
       
    11   - markup for bound variables
       
    12   - markup for types of term variables (e.g. displayed as tooltips)
     8 
    13 
     9 * Rule attributes in local theory declarations (e.g. locale or class)
    14 * Rule attributes in local theory declarations (e.g. locale or class)
    10 are now statically evaluated: the resulting theorem is stored instead
    15 are now statically evaluated: the resulting theorem is stored instead
    11 of the original expression.  INCOMPATIBILITY in rare situations, where
    16 of the original expression.  INCOMPATIBILITY in rare situations, where
    12 the historic accident of dynamic re-evaluation in interpretations
    17 the historic accident of dynamic re-evaluation in interpretations