Re: [isabelle] attributes associated with a lemma/theorem

On Wed, 21 Jan 2009, Christian Sternagel wrote:

> Is it possible to print all the attributes that are currently set for a 
> given theorem? I only found `print_attributes', but that doesn't take 
> any argument, does it?

Attributes are essentially functions that operate on theorems (and the 
implicit context), e.g. "simp" to add a thm to the part of the context 
where the Simplifier looks later.  These tools usually provide ways to 
inspect this aspect of the context, e.g. 'print_simpset'.

Projecting the content of the universal context like that is the only way 
to get to the desired information.  In particular, attributes are not like 
"tags" sticking to a theorem.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.