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

[Lawrence Paulson]

That is an entirely different situation. It’s used as test data. Nobody will get confused or distracted by that.

Larry
On 11 Jan 2023 at 11:41 +0000, Makarius <makarius at sketis.net>, wrote:
On 11/01/2023 11:54, Lawrence Paulson wrote:
Fortunately, there is not a single use of BigO anywhere in the AFP.
Let’s delete it altogether.

What do you intend to do with its clone in src/HOL/Metis_Examples ?


Makarius

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230111/b0e89a79/attachment.htm>