Re: [isabelle] Tips to make a simplification simpler?
Le Tue, 31 Jul 2012 08:08:31 +0200, Tobias Nipkow
<nipkow at in.tum.de> a écrit:
The message "simp_trace_depth_limit exceeded!" merely tells you that the
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
depth has been exceeded. The behaviour of the simplifier is not affected,
its tracing is stopped until it emerges from its recursive invocations.
a very simpled-minded way of getting a abstract view of the trace. If
more tracing info, you can always increase the limit - in ProofGeneral
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and