Alethe

[Makarius]

On 02/10/2026 23:02, Makarius 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.
I have spent 5 more minutes o Alethe: there are approx. 10 relatively small 
.thy files, most of them could be just one Alethe.thy and another one for 
Alethe_Real.thy, for example. This is not relevant for the release, and won't 
happen now.

After the release we shall have an appointment with Hanna Lachnit to sort out 
various questions. Notably about generated sources by the IsaRARE tool, the 
use of 'named_theorems" etc.


	Makarius