[isabelle-dev] simplifier trace (and jedit)
nipkow at in.tum.de
Wed May 23 10:16:54 CEST 2012
Am 23/05/2012 06:15, schrieb Christian Sternagel:
> - in the "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
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