| changeset 62343 | 24106dc44def |
| parent 61830 | 4f5ab843cf5b |
| child 63648 | f9f3006a5579 |
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Wed Feb 17 21:51:55 2016 +0100 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Wed Feb 17 21:51:56 2016 +0100 @@ -115,10 +115,7 @@ text\<open>Added to extend initstate with set of nonces\<close> lemma parts_image_Nonce [simp]: "parts (Nonce`N) = Nonce`N" -apply auto -apply (erule parts.induct) -apply auto -done + by auto lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" apply (unfold keysFor_def)