Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed junk;
authorwenzelm
Sun, 20 May 2018 22:04:17 +0200
changeset 68237 e7c85e2dc198
parent 68236 b4484ec4a8f7
child 68238 eb57621568bb
removed junk;
src/Doc/Tutorial/Protocol/Message.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle