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. Tjark _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
