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

Lawrence Paulson lp15 at cam.ac.uk
Wed Feb 26 11:52:41 CET 2020

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

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>

More information about the isabelle-dev mailing list