Am 23/05/2012 06:15, schrieb Christian Sternagel:
- in the [1]Rewriting: messages, we actually just see the redex and the
contractum, but not the context of a rewrite step. Why not show the whole
terms?
(One reason against this is the high redundancy and potentially huge size of
such traces,
I am amazedby you and the simplifier!
Yes, indeed one rule in question was added by mksimps.
You were spot on. I never knew that they have some
more-than-special meaning. ;o)
The reason why I prefer to keep the freshness constraints
together is that
atom a # (x1, x2, x3, x4, x5)
would
On Tue, 22 May 2012, Christian Urban wrote:
Assuming that this is about the bowels of the simplifier,
I hope this is the right place to ask the following question.
From what I've seen on the thread so far, it is all perfectly normal
Isabelle user-space. You did not propose to re-implement
On Wed, 23 May 2012, Christian Sternagel wrote:
3) Furthermore, in my course I recommend students (which know about term
rewriting before) to have a look at the simplifier trace whenever the
simplifier does something unexpected or does not terminate. However, for
the latter use-case (i.e.,
On 05/23/2012 10:38 PM, Makarius wrote:
On Wed, 23 May 2012, Christian Sternagel wrote:
3) Furthermore, in my course I recommend students (which know about
term rewriting before) to have a look at the simplifier trace whenever
the simplifier does something unexpected or does not terminate.
