[isabelle-dev] docs for new datatype package
makarius at sketis.net
Wed Apr 22 15:02:49 CEST 2015
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.
More information about the isabelle-dev