changeset 76290 | 64d29ebb7d3d |
parent 76289 | a6cc15ec45b2 |
child 81248 | 8205db6977dd |
--- a/src/HOL/Auth/Public.thy Thu Oct 13 16:00:22 2022 +0100 +++ b/src/HOL/Auth/Public.thy Thu Oct 13 16:09:31 2022 +0100 @@ -255,7 +255,7 @@ that expression is not in normal form.\<close> lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" -apply (unfold keysFor_def) +unfolding keysFor_def apply (induct_tac "C") apply (auto intro: range_eqI) done