Re: [isabelle] Documentation on the simplifier

On Tue, 21 Sep 2010, Steve W wrote:

Does anyone know if there's any documentation on how the simplifier works? It'd be good if it covers both the theoretical and implementation aspects. I've tried tracing the ML code, but there are quite a few functions involved and they aren't documented unfortunately.

Chapter 9 of the old "ref" manual of Isabelle gives some explanations that are not totally outdated.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.