[isabelle-dev] NEWS: attributes

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

- Brian

More information about the isabelle-dev mailing list