Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Removing a lemma or locale from a theory

Email Gateway (Aug 19 2022 at 08:33):

From: John Munroe <munddr@gmail.com>
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

Last updated: Nov 21 2024 at 12:39 UTC