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

Makarius makarius at sketis.net
Wed Jan 11 12:41:30 CET 2023

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 ?


More information about the isabelle-dev mailing list