Re: [isabelle] Isabelle Foundation & Certification
I was under the impression that this patch had been adopted. I donât believe that I saw any arguments against it.
> On 16 Sep 2015, at 15:38, Peter Lammich <lammich at in.tum.de> wrote:
> In the replied-to mail, I see more arguments that we should add proper
> dependency checking to Isabelle/HOL as soon as possible.
> As far as I know, there is a patch of KunÄar, which exists for more than
> half a year now, which
> * ensures that consts/defs only produce conservative extensions
> * Does not slow down Isabelle significantly
> * Works with whole AFP and Isabelle-Library, i.e., is does not break
> existing formalizations by being too restrictive.
> However, it seems to be rejected or not given high priority by some main
> Isabelle developers.
This archive was generated by a fusion of
Pipermail (Mailman edition) and