[isabelle] Documentation on the simplifier

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.


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