--- 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