[isabelle-dev] Fwd: A possible bug with Isabelle 2013

Lawrence Paulson lp15 at cam.ac.uk
Tue Feb 26 17:37:15 CET 2013


That mysterious type always throws me.

I guess you are saying that this dangling type dependence introduces a function type in the first line. Unfortunately, this is a difficult matter to explain to a student. I'll just have to tell him to constrain the types of his bound variables. I believe that the type of X may also be to blame.

Larry

On 26 Feb 2013, at 16:27, Tobias Nipkow <nipkow at in.tum.de> wrote:

> The two y's are given separate types. In fact, Isabelle introduces ??'a itself
> in the process.




More information about the isabelle-dev mailing list