[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?

Thanks,
-john




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