[isabelle-dev] docs for new datatype package

[Makarius]

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