[isabelle] Removing a lemma or locale from a theory



Hi,

I see that a lemma, locale, etc. can be 'removed' from a theory via
undoing. However, are there (theoretical) ramifications if a lemma,
locale, etc. is removed internally via ML? Does Isabelle try to
enforce or maintain some kind of monotonicity in terms of the elements
in a theory?

Thanks

John





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