[isabelle] Tracing intro and elim in auto
I'd like to see which intro and elim rules are applied when auto tries
to find a proof (including the rules that are not used in the final
proof, but were tried before auto back tracked).
I know that for the simplifier there is the option simp_trace, but I
can't find an option for what I want (rule_trace, smt_trace, metis_trace
all do other things). Is there an option that I missed?
This archive was generated by a fusion of
Pipermail (Mailman edition) and