Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Examining the steps taken by auto


view this post on Zulip Email Gateway (Aug 18 2022 at 15:14):

From: Creighton Hogg <wchogg@gmail.com>
Hello,

I'm still pretty new to Isabelle, and I have an example of a theorem that
'auto' can solve with the appropriate intro rules added, but I'm not sure
how auto actually did it! Is there a way in Isabelle/Proof General to print
out the chain of rules that auto found to apply?

Cheers,


Last updated: Apr 25 2024 at 16:19 UTC