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 <[email protected]>, wrote: > > Apparently we do, in src/HOL/Analysis/Borel_Space.thy. > > Don't ask me why. Yes, it should be moved.
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
