--- a/src/HOL/Auth/Message.thy Fri Oct 14 14:57:48 2022 +0100
+++ b/src/HOL/Auth/Message.thy Fri Oct 14 15:48:31 2022 +0100
@@ -65,7 +65,7 @@
"keysFor H == invKey ` {K. \<exists>X. Crypt K X \<in> H}"
-subsubsection\<open>Inductive Definition of All Parts" of a Message\<close>
+subsection\<open>Inductive Definition of All Parts of a Message\<close>
inductive_set
parts :: "msg set \<Rightarrow> msg set"
@@ -96,13 +96,13 @@
by auto
-subsubsection\<open>Inverse of keys\<close>
+subsection\<open>Inverse of keys\<close>
lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
by (metis invKey)
-subsection\<open>keysFor operator\<close>
+subsection\<open>The @{term keysFor} operator\<close>
lemma keysFor_empty [simp]: "keysFor {} = {}"
unfolding keysFor_def by blast