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