[isabelle] Tracing intro and elim in auto



Hi,

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?

Thanks,
Kyndylan




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.