Fwd: Alethe

[Makarius]

-------- 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