diff -r b45c8e35231e -r e4fa45571bab src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Tue Oct 18 15:59:15 2022 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed Oct 19 13:39:00 2022 +0100
@@ -19,9 +19,9 @@
 by blast
 
 text\<open>Collapses redundant cases in the huge protocol proofs\<close>
-lemmas disj_simps = disj_comms disj_left_absorb disj_assoc 
+lemmas disj_simps = disj_comms disj_left_absorb disj_assoc
 
-text\<open>Effective with assumptions like \<^term>\<open>K \<notin> range pubK\<close> and 
+text\<open>Effective with assumptions like \<^term>\<open>K \<notin> range pubK\<close> and
    \<^term>\<open>K \<notin> invKey`range pubK\<close>\<close>
 lemma notin_image_iff: "(y \<notin> f`I) = (\<forall>i\<in>I. f i \<noteq> y)"
 by blast
@@ -85,7 +85,7 @@
 
 text\<open>The function is indeed injective\<close>
 lemma inj_nat_of_agent: "inj nat_of_agent"
-by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split) 
+by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split)
 
 
 definition
@@ -620,16 +620,6 @@
 apply (erule analz.induct, blast+)
 done
 
-(*These two are obsolete (with a single Spy) but cost little to prove...*)
-lemma analz_UN_analz_lemma:
-     "X\<in> analz (\<Union>i\<in>A. analz (H i)) ==> X\<in> analz (\<Union>i\<in>A. H i)"
-apply (erule analz.induct)
-apply (blast intro: analz_mono [THEN [2] rev_subsetD])+
-done
-
-lemma analz_UN_analz [simp]: "analz (\<Union>i\<in>A. analz (H i)) = analz (\<Union>i\<in>A. H i)"
-by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD])
-
 
 subsection\<open>Inductive relation "synth"\<close>
 
@@ -760,7 +750,7 @@
 done
 
 lemma Fake_parts_insert_in_Un:
-     "[|Z \<in> parts (insert X H);  X \<in> synth (analz H)|] 
+     "[|Z \<in> parts (insert X H);  X \<in> synth (analz H)|]
       ==> Z \<in>  synth (analz H) \<union> parts H"
 by (blast dest: Fake_parts_insert [THEN subsetD, dest])