[isabelle] attribute 'standard'
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