[isabelle-dev] NEWS: attributes
makarius at sketis.net
Sun Nov 20 21:52:17 CET 2011
* Rule attributes in local theory declarations (e.g. locale or class)
are now statically evaluated: the resulting theorem is stored instead
of the original expression. INCOMPATIBILITY in rare situations, where
the historic accident of dynamic re-evaluation in interpretations
etc. was exploited.
* Commands 'lemmas' and 'theorems' allow local variables using 'for'
declaration, and results are standardized before being stored. Thus
old-style "standard" after instantiation or composition of facts
becomes obsolete. Minor INCOMPATIBILITY, due to potential change of
indices of schematic variables.
This refers to Isabelle/13b101cee425.
More information about the isabelle-dev