[isabelle-dev] Datatype alt_names

Makarius makarius at sketis.net
Fri Nov 5 16:06:20 CET 2010

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.


More information about the isabelle-dev mailing list