# HG changeset patch # User wenzelm # Date 1526846657 -7200 # Node ID e7c85e2dc1988646a33c069e91c6a59b3fa6c572 # Parent b4484ec4a8f78d155dddd7aeab23a83af693fa74 removed junk; diff -r b4484ec4a8f7 -r e7c85e2dc198 src/Doc/Tutorial/Protocol/Message.thy --- a/src/Doc/Tutorial/Protocol/Message.thy Sun May 20 21:12:23 2018 +0200 +++ b/src/Doc/Tutorial/Protocol/Message.thy Sun May 20 22:04:17 2018 +0200 @@ -785,8 +785,6 @@ 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' @@ -795,8 +793,6 @@ 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