[isabelle] attribute 'standard'

Hi there,

from the ISAR reference manual I do not really get the meaning of the attribute 'standard'... the reason why I'm asking is the following:

I observed that transitivity of _^* is applied automatically, but I didn't find any [simp] declaration that would explain this to me. No I have my own closure operation on sets that is also transitive and I would like transitivity to be applied automatically to. So how do I set up a corresponding lemma (and how was it down for _^*)?



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