Re: [isabelle] Verify the legitimacy of a proof?

On 08/07/17 13:01, Manuel Eberl wrote:
> Unfortunately, it is very easy to circumvent this. I don't recall who
> found this originally, but you can hide the âtaintâ of a theorem by
> going through a type class instantiation:

"Found this originally" sounds very funny to me.

Of course, the problem of oracles vs. type classes instantiations is as
old as oracles and type class instantiations in Isabelle. It is rather
well-known for insiders.

So we are back to the new meta-problem from recent years: even power
users don't know anymore what Isabelle is and what it does, and
especially what it does not.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.