Sean McLaughlin wrote:
OK. But note that things are not a simple as that. In general, theorems added to the context are instances of theorems stored in the locale. Additionally, if the theorem was generated via interpretation (commands interpretation and interpret) its hypotheses are replaced by hypotheses of the context.