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 in.tum.de
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 http://www.in.tum.de/~berghofe
This archive was generated by a fusion of
Pipermail (Mailman edition) and