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
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
