On Sat, 13 Jul 2013, Tjark Weber wrote:
On Fri, 2013-07-12 at 19:41 +0200, Makarius wrote:
How would "Omega Algebras" fare with notation A\<^sup>\<infinity> instead
of A\<^sup>\<omega>?
Worse. Of course, a name is just that, but for clarity and convenience,
it is nice to be able to call things in Isabelle what they are called in
the literature. For serious output (e.g., papers), A\<^sup>\<infinity>
instead of A\<^sup>\<omega> would demand further post-processing.
Printing papers is yet a slightly different thing. One could play the
usual "LaTeX sugar" tricks just for output, with alternative notation
etc., or postprocess sources via some bits of perl in the document/build
script (which is optional, and not there by default).
We should get a feeling for the tendency of the move. At the start of the
thread I claimed that \<^sup>LETDIG tends to be used in postfix notation,
so the idea was to allow only \<^sub>LETDIG in identifiers.
Some people had a feeling that symmetry is better, and the empirical check
revealed that \<omega> happens to be the only letter in conflict --
superscripted digits are usually done with old-fashioned \<twosuperior>
etc. (In fact, the use of \<omega> is like that of a special numeral
here.)
I am presently tending towards the symmetric sub/sup version, since it is
a bit more conservative.
If we would go the other way, there would be also a reason to discontinue
\<twosuperior> etc. eventually, but I did not intend such a reform right
now.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
