3

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 e.g. the classical reasoner?

Gergely
  • 6,879
  • 6
  • 25
  • 35
  • 1
    Maybe unrelated. but there is the `apply_trace` method from the l4.verified project: https://stackoverflow.com/a/26827242/2743088 – haansn08 May 16 '22 at 11:52

0 Answers0