src/HOL/Auth/Public.thy
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>