[isabelle-dev] [isabelle] strict_mono with an explicit set

[Lawrence Paulson]

Thanks, I’ll see what I can do. Ideally, the old versions should be abbreviations but I won’t attempt that all at once.

Larry
On 25 Feb 2020, 17:45 +0000, Manuel Eberl <eberlm at in.tum.de>, wrote:
>
> Apparently we do, in src/HOL/Analysis/Borel_Space.thy.
>
> Don't ask me why. Yes, it should be moved.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200226/728f95d8/attachment.html>