Alethe

[Jasmin Blanchette]

> At this stage of the release process we should also concentrate on really important things, like the Sledgehammer observations by Peter Lammich 01-Oct-2026 (RC2).

Indeed. I'm looking into the Sledgehammer issue.

Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/staff/jasmin-blanchette


> On 2. Oct 2026, at 23:02, Makarius <makarius at sketis.net> wrote:
> 
> -------- Forwarded Message --------
> Subject: Re: Alethe
> Date: Fri, 2 Oct 2026 23:00:29 +0200
> From: Makarius <makarius at sketis.net>
> To: Lawrence Paulson <lp15 at cam.ac.uk>, Lawrence Paulson via isabelle-dev <isabelle-dev at proof.cit.tum.de>
> 
> On 02/10/2026 18:00, Lawrence Paulson via isabelle-dev wrote:
>> I am looking forward to the new support for CVC5 through Alethe. But could all those files be put in their own directory before the freeze tomorrow? We are putting up with 12 BNF files in the top level directory, but we don't need to do this again.
> You probably mean the many .thy files of the HOL session: this is the proper representation of its structure. I count session sub directories with theories here and there as a bad thing --- it introduces an uncertainty what the sources really are, and also makes the session hard to browse.
> 
> At this stage of the release process we should also concentrate on really important things, like the Sledgehammer observations by Peter Lammich 01-Oct-2026 (RC2).
> 
> 
> 	Makarius
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20261005/18787209/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 2707 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20261005/18787209/attachment.bin>