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

[Makarius]

On 11/01/2023 12:48, Lawrence Paulson wrote:
> That is an entirely different situation. It’s used as test data. Nobody will 
> get confused or distracted by that.

I find it confusing to have a clone with its original lost in time and space.

If you want to avoid general user confusion, the traditional approach is to 
move it into the "HOL-ex" bin.


	Makarius