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

[Alexander Krauss]

Lawrence Paulson wrote:
> The simplicity of the new code compared with the old suggests that 
> this treatment is easier to understand, so we should give it a try.

My feeling is also that it would produce less surprises than the current
version.

An incompatibility that will not be reported by tests is that
intermediate goal states, where nonzero indexnames are quite frequent,
will look significantly different and contain many dots. At least we
should be aware of that, and probably should look at a few realistic 
goal states to see what this means in practice.


Makarius wrote:
> 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.)

I don't really know what conceptual advances could be expected here. 
Normally, saved results are already "standardized" by the infrastructure 
(except in the case that was pointed out), so there the indexnames are 
zeroed. With the proposed change, zero indexnames are always printed 
directly, which is in fact quite close to "avoiding the printing of 
indexnames altogether".

Alex