changeset 76288 | b82ac7ef65ec |
parent 76287 | cdc14f94c754 |
child 76289 | a6cc15ec45b2 |
--- a/src/HOL/Auth/Public.thy Thu Oct 13 15:38:32 2022 +0100 +++ b/src/HOL/Auth/Public.thy Thu Oct 13 15:49:09 2022 +0100 @@ -95,7 +95,7 @@ by blast lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)" -by (unfold symKeys_def, auto) + unfolding symKeys_def by (auto) lemma analz_symKeys_Decrypt: "\<lbrakk>Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H\<rbrakk>