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

Lawrence Paulson lp15 at cam.ac.uk
Wed Jan 11 11:54:55 CET 2023

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.

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>

More information about the isabelle-dev mailing list