Re: [isabelle] Documentation on the simplifier

At the Isabelle Developers Workshop in 2009
(, Stefan Berghofer described the
basics of how one would go about (re)implementing the simplifier.

It's not a description of the theory, but the Isabelle theory file
( provides a nice
description of conversionals and they can be composed to build up
something like the simplifier.

For some theory about rewriting, I like "Term Rewriting and All That" by
Baarder and Nipkow.


Steve W wrote:
> Hi all,
> 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.
> Thanks,
> Steve

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

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