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

Lawrence Paulson lp15 at cam.ac.uk
Wed Jan 11 12:48:20 CET 2023

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

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 ?


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

More information about the isabelle-dev mailing list