[isabelle-dev] AFP/HLDE

Christian Sternagel c.sternagel at gmail.com
Tue Oct 9 10:57:03 CEST 2018

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.



More information about the isabelle-dev mailing list