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

Best regards,
Jeremy

-- 
____________________________________
Jeremy Siek <jeremy.siek at colorado.edu>
http://ecee.colorado.edu/~siek/
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.