> On 11 Jan 2023, at 04:52, Makarius <makarius at sketis.net> wrote: > > So the ultra-short answer to this thread might just be: move Big_O from HOL-Library to HOL-ex. I like that idea. Cheers, Gerwin