NEWS
changeset 14257 a7ef3f7588c5
parent 14255 e6e3e3f0deed
child 14283 516358ca7b42
equal deleted inserted replaced
14256:33e5ef9a4c98 14257:a7ef3f7588c5
    38     For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
    38     For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
    39     emulations.
    39     emulations.
    40   - INCOMPATIBILITY: names of variables to be instantiated may no
    40   - INCOMPATIBILITY: names of variables to be instantiated may no
    41     longer be enclosed in quotes.  Instead, precede variable name with `?'.
    41     longer be enclosed in quotes.  Instead, precede variable name with `?'.
    42     This is consistent with the instantiation attribute "where".
    42     This is consistent with the instantiation attribute "where".
       
    43 
       
    44 * Attributes "where" and "of":
       
    45   Now take type variables of instantiated theorem into account when reading
       
    46   the instantiation string.  This fixes a bug that caused instantiated
       
    47   theorems to have too special types in some circumstances.
    43 
    48 
    44 * Locales:
    49 * Locales:
    45   - Goal statements involving the context element "includes" no longer
    50   - Goal statements involving the context element "includes" no longer
    46     generate theorems with internal delta predicates (those ending on
    51     generate theorems with internal delta predicates (those ending on
    47     "_axioms") in the premise.
    52     "_axioms") in the premise.