| changeset 76290 | 64d29ebb7d3d |
| parent 69597 | ff784d5a5bfb |
| child 76299 | 0ad6f6508274 |
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Thu Oct 13 16:00:22 2022 +0100 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Thu Oct 13 16:09:31 2022 +0100 @@ -118,7 +118,7 @@ by auto lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" -apply (unfold keysFor_def) +unfolding keysFor_def apply (induct_tac "C", auto) done