[isabelle-dev] simplifier trace (and jedit)

[Tobias Nipkow]

Am 23/05/2012 06:15, schrieb Christian Sternagel:
> - in the "[1]Rewriting:" messages, we actually just see the redex and the
> contractum, but not the context of a rewrite step. Why not show the whole terms?
> (One reason against this is the high redundancy and potentially huge size of
> such traces, but on the other hand, they are traces and only generated when
> requested.)

Size is indeed an issue, but also that it would be a considerable amount of work
to implement it properly. Ideally you want an interactive tracer anyway, which
is yet more work.

Tobias