Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip 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: Mar 28 2024 at 08:18 UTC