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

Tjark Weber webertj at in.tum.de
Tue Feb 26 17:49:37 CET 2013

On Tue, 2013-02-26 at 16:37 +0000, Lawrence Paulson wrote:
> I guess you are saying that this dangling type dependence introduces a
> function type in the first line.

It does; you can write

  term "..."

after the first proof step to see this more explicitly.


More information about the isabelle-dev mailing list