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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
