# HG changeset patch
# User haftmann
# Date 1265811241 -3600
# Node ID 6cdf9bbd03424f9485b4ad594ebfe6ca52ab9ca4
# Parent  a0e89e47b083e524f2e2e3f2cdb0984dfedb4226
minor metis proof tuning

diff -r a0e89e47b083 -r 6cdf9bbd0342 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Wed Feb 10 14:12:40 2010 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Wed Feb 10 15:14:01 2010 +0100
@@ -252,7 +252,7 @@
 
 declare [[ atp_problem_prefix = "Message__parts_cut" ]]
 lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
-by (metis Un_subset_iff insert_subset parts_increasing parts_trans) 
+by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
 
 
 
@@ -698,13 +698,12 @@
 apply (rule subsetI)
 apply (erule analz.induct)
 apply (metis UnCI UnE Un_commute analz.Inj)
-apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Fst analz_increasing analz_mono insert_absorb insert_subset)
-apply (metis MPair_synth UnCI UnE Un_commute Un_upper1 analz.Snd analz_increasing analz_mono insert_absorb insert_subset)
+apply (metis MPair_synth UnCI UnE Un_commute analz.Fst analz.Inj mem_def)
+apply (metis MPair_synth UnCI UnE Un_commute analz.Inj analz.Snd mem_def)
 apply (blast intro: analz.Decrypt)
 apply blast
 done
 
-
 declare [[ atp_problem_prefix = "Message__analz_synth" ]]
 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
 proof (neg_clausify)