# HG changeset patch
# User paulson
# Date 874678284 -7200
# Node ID f677f0bc1cdf797143af2bb6861fd55bd494480e
# Parent  aafe719dff147845be667e7ebec932a6f0bf7f93
Deleted the obsolete theorem analz_UN1_synth

diff -r aafe719dff14 -r f677f0bc1cdf src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Thu Sep 18 13:24:04 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Fri Sep 19 16:11:24 1997 +0200
@@ -689,22 +689,6 @@
 qed "analz_synth";
 Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
 
-(*Hard to prove; still needed now that there's only one Spy?*)
-goal thy "analz (UN i. synth (H i)) = \
-\         analz (UN i. H i) Un (UN i. synth (H i))";
-by (rtac equalityI 1);
-by (rtac subsetI 1);
-by (etac analz.induct 1);
-by (blast_tac
-    (!claset addIs [impOfSubs synth_increasing,
-                    impOfSubs analz_mono]) 5);
-by (Blast_tac 1);
-by (blast_tac (!claset addIs [analz.Inj RS analz.Fst]) 1);
-by (blast_tac (!claset addIs [analz.Inj RS analz.Snd]) 1);
-by (blast_tac (!claset addIs [analz.Decrypt]) 1);
-qed "analz_UN1_synth";
-Addsimps [analz_UN1_synth];
-
 
 (** For reasoning about the Fake rule in traces **)