[isabelle-dev] NEWS: attributes
brianh at cs.pdx.edu
Tue Nov 22 15:38:13 CET 2011
On Sun, Nov 20, 2011 at 9:52 PM, Makarius <makarius at sketis.net> wrote:
> * 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.
The "standard" attribute will also generalize free type variables, for example:
lemmas bar = foo [where 'a="'b list", standard]
How can the same be accomplished with "for"? It seems not to support
More information about the isabelle-dev