Re: [isabelle-dev] Probable bug in let_simp simproc

2011-08-11 Thread Makarius
On Thu, 11 Aug 2011, Thomas Sewell wrote: 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

[isabelle-dev] Probable bug in let_simp simproc

2011-08-10 Thread Thomas Sewell
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