[isabelle-dev] Datatype alt_names
makarius at sketis.net
Fri Nov 5 16:06:20 CET 2010
On Wed, 3 Nov 2010, Christian Urban wrote:
> This naming scheme is not very user-friendly.
> So I decided to allow
> nominal_datatype (bar)
> foo1 = ..
> and foo2 = ..
> and foon = ..
> to produce
> 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