src/Doc/Tutorial/Protocol/Message.thy

     be pulled out using the @{text analz_insert} rules\<close>
 
 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" "Hash X"]
   insert_commute [of "Key K" "MPair X Y"]
   insert_commute [of "Key K" "Crypt X K'"]
   for K C N X Y K'
 
 lemmas pushCrypts =
   insert_commute [of "Crypt X K" "Agent C"]
   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" "Hash X'"]
   insert_commute [of "Crypt X K" "MPair X' Y"]
   for X K C N X' Y
 
 text\<open>Cannot be added with @{text "[simp]"} -- messages should not always be
   re-ordered.\<close>