On Tue, 8 Feb 2011, Brian Huffman wrote:
The *_tac-style instantiation might be out of fashion, but the same
parsing rules for indexnames are also used with the "where" attribute,
which is still quite useful.
In fact, the "where" attribute has its own "embrace-and-extend" version of
Larry's standard of 25+ years, and I can't say on the spot what are the
fine points of it. When inspecting these things some years ago, I added
various comments like "FIXME" and "cleanup this mess!!!" here and there.
Instead of peep-whole tuning of such old custums, I would rather like to
see some conceptual advances. E.g. the user writes down rule statements
in a certain format, and later is exposed to internal
machine-representation of index names. How can this be addressed at a
more conceptual level? How can printing of indexnames be avoided
altogether? (Without low-level tweaking like show_question_marks.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
