[isabelle-dev] Problem with simproc enat_eq_cancel

Lars Noschinski noschinl at in.tum.de
Fri Mar 1 16:30:26 CET 2013

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

More information about the isabelle-dev mailing list