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 problem.

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 problem was.


isabelle-dev mailing list

Reply via email to