# HG changeset patch
# User bulwahn
# Date 1309272224 -7200
# Node ID eb64d8e00a62ef24104da9920958896fffec811e
# Parent  ea959ab7bbe31d5f662811d9dbb4390e20b83923# Parent  027dc42505bef8ac1013d751cbf24bbe307eafbc
merged

diff -r ea959ab7bbe3 -r eb64d8e00a62 src/HOL/Auth/CertifiedEmail.thy
--- a/src/HOL/Auth/CertifiedEmail.thy	Tue Jun 28 14:36:43 2011 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy	Tue Jun 28 16:43:44 2011 +0200
@@ -197,10 +197,7 @@
 txt{*Message 2*}
 apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs)
 txt{*Message 3*}
-apply (frule_tac hr_form, assumption)
-apply (elim disjE exE) 
-apply (simp_all add: parts_insert2)
-apply (blast intro: subsetD [OF parts_mono [OF Set.subset_insertI]])  
+apply (metis parts_insertI)
 done
 
 lemma Spy_dont_know_RPwd [rule_format]:
@@ -226,8 +223,7 @@
 
 lemma Spy_analz_RPwd_iff [simp]:
     "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(spies evs)) = (A\<in>bad)"
-by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts [THEN subsetD]])
-
+by (metis Spy_know_RPwd_iff Spy_spies_bad_shrK analz.Inj analz_into_parts)
 
 text{*Unused, but a guarantee of sorts*}
 theorem CertAutenticity:
@@ -308,8 +304,7 @@
 apply (clarsimp, blast)
 txt{*Message 2*}
 apply (simp add: parts_insert2, clarify) 
-apply (drule parts_cut, assumption, simp) 
-apply (blast intro: usedI) 
+apply (metis parts_cut Un_empty_left usedI)
 txt{*Message 3*} 
 apply (blast dest: Notes_SSL_imp_used used_parts_subset_parts) 
 done