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

[Lawrence Paulson]

Since we describe that directory as “miscellaneous examples”, anything we put there needs to be presentable, so the theory will require a bit of tidying up.

Larry
On 11 Jan 2023 at 13:08 +0000, Makarius <makarius at sketis.net>, wrote:
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


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230111/b3d74321/attachment.htm>