src/HOL/Auth/Guard/Extensions.thy

 
 subsubsection{*lemmas on parts, synth and analz*}
 
 lemma parts_invKey [rule_format,dest]:"X:parts {Y} ==>
 X:analz (insert (Crypt K Y) H) --> X ~:analz H --> Key (invKey K):analz H"
-by (erule parts.induct, (fastforce dest: parts.Fst parts.Snd parts.Body)+)
+by (erule parts.induct, auto dest: parts.Fst parts.Snd parts.Body)
 
 lemma in_analz: "Y:analz H ==> EX X. X:H & Y:parts {X}"
 by (erule analz.induct, auto intro: parts.Fst parts.Snd parts.Body)
 
 lemmas in_analz_subset_parts = analz_subset_parts [THEN subsetD]
 
 lemma Crypt_synth_insert: "[| Crypt K X:parts (insert Y H);
 Y:synth (analz H); Key K ~:analz H |] ==> Crypt K X:parts H"
-apply (drule parts_insert_substD [where P="%S. Crypt K X : S"], clarify)
+apply (drule parts_insert_substD, clarify)
 apply (frule in_sub)
 apply (frule parts_mono)
-by auto
+apply auto
+done
 
 subsubsection{*greatest nonce used in a message*}
 
 fun greatest_msg :: "msg => nat"
 where