[isabelle-dev] simplifier trace (and jedit)

Tobias Nipkow nipkow at in.tum.de
Wed May 23 10:16:54 CEST 2012

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.


More information about the isabelle-dev mailing list