Email Gateway (Aug 18 2022 at 15:33): Email Gateway (Aug 18 2022 at 15:33):From: Makarius <makarius@sketis.net>
Isabelle2009-2 is now available.
This release improves upon Isabelle2009-1 in many respects, see the
NEWS file in the distribution for more details. Some notable changes
are:
Explicit proof terms for type class reasoning.
Robust treatment of concrete syntax for different logical entities;
mixfix syntax in local proof context.
Type declarations and notation within local theory context.
HOL: package for quotient types.
HOL code generation: simple concept for abstract datatypes obeying
invariants (e.g. red-black trees).
HOL: new development of the Reals using Cauchy Sequences.
HOL: reorganization of abstract algebra type class hierarchy.
HOL: substantial reorganization of main library and related tools.
HOLCF: reorganization of 'domain' package.
You may get Isabelle2009-2 from the following mirror sites:
Cambridge (UK) http://www.cl.cam.ac.uk/research/hvg/Isabelle/
Munich (Germany) http://isabelle.in.tum.de/
Sydney (Australia) http://mirror.cse.unsw.edu.au/pub/isabelle/
Email Gateway (Aug 18 2022 at 15:35):From: Joachim Breitner <mail@joachim-breitner.de>
Hi,
darn, and I just finished my APF submission. Guess I’ll have to migrate
that first to 2009-2 :-)
I’m using i3p, but this does not accept 2009-2 yet, it seems (starting
the prover does nothing). Can anyone else confirm that? Will I need to
wait for another i3p release until I can work again, or is there an easy
fix?
Thanks,
Joachim
signature.asc
Last updated: Apr 30 2024 at 08:19 UTC