# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1666183302 -3600
# Node ID 9e1fef7b4f29ae3f6c7f86c72acb1e5ac1b08dc0
# Parent  e4fa45571bab69b8382d2207185d7098f39fb0e2
deleted unused material

diff -r e4fa45571bab -r 9e1fef7b4f29 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Wed Oct 19 13:39:00 2022 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Wed Oct 19 13:41:42 2022 +0100
@@ -542,16 +542,6 @@
 apply (erule analz.induct, blast+)
 done
 
-text\<open>These two are obsolete (with a single Spy) but cost little to prove...\<close>
-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>