src/HOL/MetisExamples/Message.thy
changeset 24759 b448f94b1c88
parent 23755 1c4672d130b1
child 25457 ba2bcae7aafd
     1.1 --- a/src/HOL/MetisExamples/Message.thy	Sat Sep 29 10:47:05 2007 +0200
     1.2 +++ b/src/HOL/MetisExamples/Message.thy	Sat Sep 29 21:39:44 2007 +0200
     1.3 @@ -702,7 +702,7 @@
     1.4  apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Fst analz_increasing analz_mono insert_absorb insert_subset)
     1.5  apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Snd analz_increasing analz_mono insert_absorb insert_subset)
     1.6  apply (blast intro: analz.Decrypt)
     1.7 -apply (metis Diff_Int Diff_empty Diff_subset_conv Int_empty_right Un_commute Un_subset_iff Un_upper1 analz_increasing analz_mono synth_increasing)
     1.8 +apply blast
     1.9  done
    1.10  
    1.11