On 11/01/2023 11:54, Lawrence Paulson wrote: > Fortunately, there is not a single use of BigO anywhere in the AFP. > Let’s delete it altogether. What do you intend to do with its clone in src/HOL/Metis_Examples ? Makarius