[isabelle] (no subject)

Hi all,

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?


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