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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
