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

Gerwin Klein kleing at unsw.edu.au
Wed Jan 11 08:59:20 CET 2023

> 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.


More information about the isabelle-dev mailing list