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