On 01.03.2013 15:10, Andreas Lochbihler wrote: > By the way, why does the failure in the simproc yield a proof error at > all? Usually, simp does not raise "Proof failed" if it gets stuck > somewhere. I guess this means that the simproc raises "Proof failed" which merely propagates through the simplifier. -- Lars