[isabelle] Order of facts to be used



Hi,

I was wondering how Isabelle determines the ordering of facts to be used.
For example:

lemma lem: "c > 0"
using ax1 ax2 ax3
by auto

How does Isabelle decide the ordering needed to solve the proof goal?

Thanks
Steve




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