[isabelle-dev] NEWS: attributes
makarius at sketis.net
Tue Nov 22 15:57:34 CET 2011
On Tue, 22 Nov 2011, Brian Huffman wrote:
> 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.
Treatment of type variables follows the usual Hindley-Milner discipline of
the Isabelle/Isar context. So in the example above, you get the result as
general wrt. types according to how 'b occurs otherwise.
Proof_Context.export does all the details -- instead of manual tinkering
with individual variables as was still common 10-15 years ago.
Here is an example in a global context:
lemmas foo = refl [where 'a = "'b list"]
(?t\<Colon>?'b list) = ?t
When doing the change, I was aware of that fine point and made some sanity
checks with common examples. It does not mean there could not be some
mistakes lurking, but all Isabelle examples and AFP were still working
More information about the isabelle-dev