[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution

[Makarius]

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