Re: [isabelle] Documentation on the simplifier
At the Isabelle Developers Workshop in 2009
(http://tphols.in.tum.de/idw.html), 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
(http://tphols.in.tum.de/IDW/Conversions.thy) 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.
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