Deleted the obsolete theorem analz_UN1_synth
authorpaulson
Fri Sep 19 16:11:24 1997 +0200 (1997-09-19)
changeset 3684f677f0bc1cdf
parent 3683 aafe719dff14
child 3685 5b8c0c8f576e
Deleted the obsolete theorem analz_UN1_synth
src/HOL/Auth/Message.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Thu Sep 18 13:24:04 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Sep 19 16:11:24 1997 +0200
     1.3 @@ -689,22 +689,6 @@
     1.4  qed "analz_synth";
     1.5  Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
     1.6  
     1.7 -(*Hard to prove; still needed now that there's only one Spy?*)
     1.8 -goal thy "analz (UN i. synth (H i)) = \
     1.9 -\         analz (UN i. H i) Un (UN i. synth (H i))";
    1.10 -by (rtac equalityI 1);
    1.11 -by (rtac subsetI 1);
    1.12 -by (etac analz.induct 1);
    1.13 -by (blast_tac
    1.14 -    (!claset addIs [impOfSubs synth_increasing,
    1.15 -                    impOfSubs analz_mono]) 5);
    1.16 -by (Blast_tac 1);
    1.17 -by (blast_tac (!claset addIs [analz.Inj RS analz.Fst]) 1);
    1.18 -by (blast_tac (!claset addIs [analz.Inj RS analz.Snd]) 1);
    1.19 -by (blast_tac (!claset addIs [analz.Decrypt]) 1);
    1.20 -qed "analz_UN1_synth";
    1.21 -Addsimps [analz_UN1_synth];
    1.22 -
    1.23  
    1.24  (** For reasoning about the Fake rule in traces **)
    1.25