src/HOL/SET_Protocol/Message_SET.thy

   The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*}
 
 lemma parts_increasing: "H \<subseteq> parts(H)"
 by blast
 
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
 
 lemma parts_empty [simp]: "parts{} = {}"
 apply safe
 apply (erule parts.induct, blast+)
 done

 lemma analz_subset_parts: "analz H \<subseteq> parts H"
 apply (rule subsetI)
 apply (erule analz.induct, blast+)
 done
 
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
-
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
+
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
 
 
 lemma parts_analz [simp]: "parts (analz H) = parts H"
 apply (rule equalityI)
 apply (rule analz_subset_parts [THEN parts_mono, THEN subset_trans], simp)

 lemma analz_parts [simp]: "analz (parts H) = parts H"
 apply auto
 apply (erule analz.induct, auto)
 done
 
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
 
 subsubsection{*General equational properties*}
 
 lemma analz_empty [simp]: "analz{} = {}"
 apply safe

 
 
 text{*Rewrites to push in Key and Crypt messages, so that other messages can
     be pulled out using the @{text analz_insert} rules*}
 
-lemmas pushKeys [standard] =
+lemmas pushKeys =
   insert_commute [of "Key K" "Agent C"]
   insert_commute [of "Key K" "Nonce N"]
   insert_commute [of "Key K" "Number N"]
   insert_commute [of "Key K" "Pan PAN"]
   insert_commute [of "Key K" "Hash X"]
   insert_commute [of "Key K" "MPair X Y"]
   insert_commute [of "Key K" "Crypt X K'"]
-
-lemmas pushCrypts [standard] =
+  for K C N PAN X Y K'
+
+lemmas pushCrypts =
   insert_commute [of "Crypt X K" "Agent C"]
   insert_commute [of "Crypt X K" "Nonce N"]
   insert_commute [of "Crypt X K" "Number N"]
   insert_commute [of "Crypt X K" "Pan PAN"]
   insert_commute [of "Crypt X K" "Hash X'"]
   insert_commute [of "Crypt X K" "MPair X' Y"]
+  for X K C N PAN X' Y
 
 text{*Cannot be added with @{text "[simp]"} -- messages should not always be
   re-ordered.*}
 lemmas pushes = pushKeys pushCrypts