[isabelle-dev] Datatype alt_names

[Makarius]

On Wed, 3 Nov 2010, Christian Urban wrote:

>  foo1_foo2_....._foon.induct
>
> This naming scheme is not very user-friendly.
> So I decided to allow
>
>  nominal_datatype (bar)
>       foo1 = ..
>  and  foo2 = ..
>       ....
>  and  foon = ..
>
> to produce
>
>  bar.induct
>
> etc instead. I do not know of anything else that would allow the user to 
> have control over the generated theorem names. Is this something which 
> goes against all Isabelle conventions? Could this be helpful for 
> "normal" datatypes?

It all reminds of of our original intentions many years ago.  I would like 
to get an idea what is implemented now in 'datatype' and 'inductive', and 
what the manuals say about it, but did not manage to find time for it yet.


 	Makarius