[isabelle-dev] NEWS: attributes

[Makarius]

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:

declare [[show_types]]
lemmas foo = refl [where 'a = "'b list"]
thm foo

(?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 
fine afterwards.


 	Makarius