[isabelle-dev] NEWS: attributes

[Brian Huffman]

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
type variables.

- Brian