[isabelle-dev] AFP/HLDE

[Christian Sternagel]

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