[isabelle] difference between "using" versus auto simp:

I've noticed that on a few occasions, referencing a lemma with
a "using" followed by auto didn't work, whereas adding the
lemma to the simp set via "auto simp:" did work.
Are there some general rules of thumb regarding when to use

Best regards,

Jeremy Siek <jeremy.siek at colorado.edu>
Assistant Professor
Dept. of Electrical, Computer, and Energy Engineering
University of Colorado at Boulder

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