proof metadata
claudio remarks:
CSC:it is typically the case that oneis interested then in recording more infos,
like the lemmas used, the depth at which the proof was found,
the length of the proof search measured in steps, etc.
This data is used to guarantee that the proof can be found again and/or for
tracking how automation is made stronger/weaker by system changes.
MW: In Isabelle, such technical data is difficult to attach to individual types, consts,
facts (with proofs): the system manages commands that may produce multiple such entities,
and timing information is only attached to the overall command transaction.