On 10/08/2018 04:14 PM, Makarius wrote: > On 08/10/18 15:58, Lars Hupel wrote: > > I don't mind if it is possible to eliminate AFP/HLDE (theory > Diophantine_Eqns_Lin_Hom.Solver_Code) outright, and just refrain from > doing such things in AFP. >
Compiling a binary in HLDE was a mere experiment on our side too. So I also do not mind much to remove this again from the AFP. I would however like to keep theory Solver_Code and still let it generate Haskell source code (that is required for the handwritten Main.hs). Then the task of setting up a proper Haskell environment and compiling an executable is moved to prospective users. Which is fine with me. cheers chris _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev