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.
Larry

> 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 MHonArc.