On 05/10/18 20:20, Christian Sternagel wrote:
>
> On 10/05/2018 07:10 PM, Makarius wrote:
>> What is the purpose of the session HLDE, with its duplicate theory
>> Solver_Code that is also in Diophantine_Eqns_Lin_Hom?
>
> As the author of the corresponding ROOT file, when I look at it now, I
> cannot think of any reason to have also session HLDE (except of course
> the shorter name).
So the question is reduced by one step: What is the purpose of theory
"Solver_Code" abstractly?
It seems to deliver an executable tool for later use elsewhere, but the
implementation is very fragile.
We could take it as a model to get such a task right.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
