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

[Makarius]

On 10/01/2023 12:56, Lawrence Paulson wrote:
> This theory is ancient and looks it. It’s also totally unused and probably 
> obsolete. Shall we delete it?

This may be answered by figuring out its uses in applications. notably AFP.

There is also a clone of it in src/HOL/Metis_Examples/Big_O.thy --- I use that 
regularly to test Isabelle/PIDE/Sledgehammer + ATPs, just because it comes 
early in the alphabet and contains some nontrivial things.


	Makarius