[isabelle-dev] Fwd: [isabelle] Problem with frule_tac substitution
krauss at in.tum.de
Wed Feb 9 09:36:37 CET 2011
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
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.
> 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
More information about the isabelle-dev