Re: [isabelle] Tips to make a simplification simpler?

Le Tue, 31 Jul 2012 08:08:31 +0200, Tobias Nipkow <nipkow at> a écrit:

The message "simp_trace_depth_limit exceeded!" merely tells you that the *trace*
depth has been exceeded. The behaviour of the simplifier is not affected,
That's what I guessed too, while was still surprised a limit was exceeded with what looked simple to me. On the other hand, I understand simplification is the most important and tedious part of proof assistance and that it easily requires more steps than what a human believe in his mind.

its tracing is stopped until it emerges from its recursive invocations. This is a very simpled-minded way of getting a abstract view of the trace. If you want more tracing info, you can always increase the limit - in ProofGeneral there is
a menue item Trace Simplifier Depth for it.

I searched for a way to have the same with jEdit. That's the opportunity of another topic.

We expect to provide better tracing facilities in the future.


May be a simple text filter would be enough. But I did not go into these internals for now.

Thanks for your comments and explanations.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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