Some time ago I asked this question on Stack Overflow but got no answer:
Section 9.4 The Classical Reasoner of the Isar Reference Manual writes:
The tactics can be traced, and their components can be called directly; in this manner, any proof can be viewed interactively.
I have found sections in this manual about tracing the simplifier and higher order unification.
How can I trace the classical reasoner?