Email Gateway (Oct 03 2021 at 19:04): Email Gateway (Oct 03 2021 at 19:04):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
the next release is scheduled for 15-Dec-2021 (or a bit earlier). The first
official release candidate will appear around 01-Nov-2021.
To warm up, here is a informal snapshot for experimentation and early
feedback: https://isabelle.sketis.net/website-Isabelle2021-1-RC0
Many things are still missing: for example there will be a proper linux-arm
distribution eventually, e.g. for docker on Apple Silicon M1.
Many other things are already there, but not yet covered in NEWS.
Makarius
Email Gateway (Oct 04 2021 at 10:26):From: Frédéric Boulanger <frederic.boulanger@centralesupelec.fr>
Hello,
It would be nice to minimise incompatibilities with the previous version by adding:
abbreviation strict_sorted :: "'a::ord list ⇒ bool" where
"strict_sorted ≡ sorted_wrt (<)"
to List.thy
I had no problem to fix the proofs that rely on strict_sorted with a call to sledgehammer.
Last updated: Jan 04 2025 at 20:18 UTC