[isabelle-dev] HOL/Library/BigO.thy

[Lawrence Paulson]

I agree with Tobias. We are already very good at preserving our past, but it’s exasperating when novices stumble across legacy material and emulate that style. Fortunately, there is not a single use of BigO anywhere in the AFP. Let’s delete it altogether.

Larry
On 11 Jan 2023 at 08:06 +0000, Tobias Nipkow <nipkow at in.tum.de>, wrote:

The distribution is meant to provide a curated set of theories. They are in
constant flux anyway. And if some theory is definitely outdated we should remove
it rather than keep it around and confuse users. For archeological purposes we
have mercurial.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230111/1fbc15cb/attachment-0001.htm>