I spent a bit of yesterday trying to discover why the standard simpset
was taking forever to simplify a large term I happen to have.
The term is folded down in such a manner that unfolding Let_def will
cause it to grow extremely large, which turns out to be what is
happening. Deleting the let_simp simproc from the simpset solves the
The let_simp simproc is written in two halves. The first bit I can
easily understand, and if I produce a simproc with just that code it
does what is expected.
The second half is commented "Norbert Schirmer's case", and is
incomprehensible to me at the moment. Does anyone know, broadly, what it
is meant to do? If I knew that I might be able to figure out what the
isabelle-dev mailing list