  The Isabelle proof assistant comes equipped with a very powerful tactic for
term simplification. While tremendously useful, the results of simplifying a
term do not always match the user's expectation: sometimes, the resulting term
is not in the form the user expected, or the simplifier fails to apply a rule.
We describe a new, interactive tracing facility which offers insight into the
hierarchical structure of the simplification with user-defined filtering,
memoization and search. The new simplifier trace is integrated into the
Isabelle/jEdit Prover IDE.
