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

[Makarius]

On 10/01/2023 18:45, Makarius wrote:
> 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.

A few more considerations:

   * We have lots of "rubbish examples", notably in HOL-ex. Traditionally we 
never really deleted old things, but rather upgraded them to the continuously 
changing system (and library). This is a distinctive strength of Isabelle. 
Sometimes it is fun to meet contributors from decades ago, and show them their 
ancient experiments.

   * We have recently introduced HOL-Examples for "prominent" or "notable" 
examples. Very little has happened so far to sort things out, i.e. to move 
more material from HOL-ex to HOL-Examples.

   * HOL-Library was originally meant as support for "prominent" or "notable" 
applications. It might have grown a bit uneven in recent years, but I can't 
tell for sure.


So the ultra-short answer to this thread might just be: move Big_O from 
HOL-Library to HOL-ex.

	Makarius