Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/Yahalom2.ML
changeset 5492 d9fc3457554e
parent 5434 9b4bed3f394c
child 5932 737559a43e71 
--- a/src/HOL/Auth/Yahalom2.ML	Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Tue Sep 15 15:10:38 1998 +0200
@@ -132,7 +132,7 @@
 (** Session keys are not used to encrypt other session keys **)
 
 Goal "evs : yahalom ==>                               \
-\  ALL K KK. KK <= Compl (range shrK) -->                \
+\  ALL K KK. KK <= - (range shrK) -->                 \
 \         (Key K : analz (Key``KK Un (spies evs))) =  \
 \         (K : KK | Key K : analz (spies evs))";
 by (etac yahalom.induct 1);
isabelle