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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
