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

Lawrence Paulson lp15 at cam.ac.uk
Wed Jan 11 17:02:47 CET 2023

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.

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.


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

More information about the isabelle-dev mailing list