Re: [isabelle] Isabelle Foundation & Certification
On Mi, 2015-09-16 at 16:10 +0100, Larry Paulson wrote:
> I was under the impression that this patch had been adopted. I donât believe that I saw any arguments against it.
If this should be true, we should make it as public as possible, to stop
any rumours about Isabelle unsoundness. The best way would be to release
Isabelle2015-1 immediately, even if it would only be (Isabelle2015 +
patch), and not based on the current state of the repository.
> > 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