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/OtwayReesBella.thy
changeset 76287 cdc14f94c754
parent 69597 ff784d5a5bfb
child 76289 a6cc15ec45b2 
--- a/src/HOL/Auth/OtwayReesBella.thy	Thu Oct 13 14:49:15 2022 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy	Thu Oct 13 15:38:32 2022 +0100
@@ -146,7 +146,7 @@
 by auto
 
 lemma Spy_see_shrK_D [dest!]:
-     "[|Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> orb|] ==> A \<in> bad"
+     "\<lbrakk>Key (shrK A) \<in> parts (knows Spy evs);  evs \<in> orb\<rbrakk> \<Longrightarrow> A \<in> bad"
 by (blast dest: Spy_see_shrK)
 
 lemma new_keys_not_used [simp]:
isabelle