Re: [isabelle] (no subject)

John Matthews wrote:
Matt Kaufmann and I are interested in how Isabelle's simplifier handles the case where there are multiple congruence rules that match a particular subterm. Does it try all the rules in some order, or does it just pick one?

The simplifier currently only allows one congruence rule per constant.
See section 10.2.6 of the Isabelle reference manual for more information.


Dr. Stefan Berghofer               E-Mail: berghofe at
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY  

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