removed junk;
authorwenzelm
Sun May 20 22:04:17 2018 +0200 (21 months ago)
changeset 68237e7c85e2dc198
parent 68236 b4484ec4a8f7
child 68238 eb57621568bb
removed junk;
src/Doc/Tutorial/Protocol/Message.thy
     1.1 --- a/src/Doc/Tutorial/Protocol/Message.thy	Sun May 20 21:12:23 2018 +0200
     1.2 +++ b/src/Doc/Tutorial/Protocol/Message.thy	Sun May 20 22:04:17 2018 +0200
     1.3 @@ -785,8 +785,6 @@
     1.4  lemmas pushKeys =
     1.5    insert_commute [of "Key K" "Agent C"]
     1.6    insert_commute [of "Key K" "Nonce N"]
     1.7 -  insert_commute [of "Key K" "Number N"]
     1.8 -  insert_commute [of "Key K" "Hash X"]
     1.9    insert_commute [of "Key K" "MPair X Y"]
    1.10    insert_commute [of "Key K" "Crypt X K'"]
    1.11    for K C N X Y K'
    1.12 @@ -795,8 +793,6 @@
    1.13    insert_commute [of "Crypt X K" "Agent C"]
    1.14    insert_commute [of "Crypt X K" "Agent C"]
    1.15    insert_commute [of "Crypt X K" "Nonce N"]
    1.16 -  insert_commute [of "Crypt X K" "Number N"]
    1.17 -  insert_commute [of "Crypt X K" "Hash X'"]
    1.18    insert_commute [of "Crypt X K" "MPair X' Y"]
    1.19    for X K C N X' Y
    1.20