On 19/10/2014 19:52, Amarin Phaosawasdi wrote:
One possibility: lemma "ev 4" using evSS[OF evSS[OF ev0]] by(simp add: numeral_eq_Suc)Thank you. Is there a difference between using a proof vs adding it to simp like this?
Yes, with "using" the fact becomes part of the proof state and is simplified itself. Tobias
lemma "ev 4" by (simp add: numeral_eq_Suc evSS[OF evSS[OF ev0]]) Amarin
Description: S/MIME Cryptographic Signature