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

[Tobias Nipkow]

The distribution is meant to provide a curated set of theories. They are in 
constant flux anyway. And if some theory is definitely outdated we should remove 
it rather than keep it around and confuse users. For archeological purposes we 
have mercurial.

Tobias

On 11/01/2023 08:59, Gerwin Klein wrote:
> 
>> On 11 Jan 2023, at 04:52, Makarius <makarius at sketis.net> wrote:
>>
>> So the ultra-short answer to this thread might just be: move Big_O from HOL-Library to HOL-ex.
> 
> I like that idea.
> 
> Cheers,
> Gerwin
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20230111/715df536/attachment.bin>