# HG changeset patch # User paulson # 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\These two are obsolete (with a single Spy) but cost little to prove...\ -lemma analz_UN_analz_lemma: - "X\ analz (\i\A. analz (H i)) ==> X\ analz (\i\A. H i)" -apply (erule analz.induct) -apply (blast intro: analz_mono [THEN [2] rev_subsetD])+ -done - -lemma analz_UN_analz [simp]: "analz (\i\A. analz (H i)) = analz (\i\A. H i)" -by (blast intro: analz_UN_analz_lemma analz_mono [THEN [2] rev_subsetD]) - subsection\Inductive relation "synth"\