On Tue, 21 Apr 2015, Gerwin Klein wrote:
I’m pretty much poking in the dark here, though. I briefly looked at the
code of the induct method and then remembered why I never wanted to do
that again..
I know what you mean. I started the "cases" and "induct" methods many
years ago, but piled up only half of the cumulative features that make it
now close to intractable.
I still do hope that the normal "convergence principle" of Isabelle
development can be applied eventually, to re-integrate the forks and
variations that have emerged in recent years. This also applies to the
relatively new "co" versions.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
