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

Makarius makarius at sketis.net
Wed Jan 11 14:08:20 CET 2023

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.


More information about the isabelle-dev mailing list