--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Wed Jan 10 15:25:09 2018 +0100
@@ -59,7 +59,7 @@
assumes "dc \<in> dining_cryptographers"
shows "result dc \<longleftrightarrow> (payer dc \<noteq> None)"
proof -
- let ?XOR = "\<lambda>f l. foldl (op \<noteq>) False (map f [0..<l])"
+ let ?XOR = "\<lambda>f l. foldl (\<noteq>) False (map f [0..<l])"
have foldl_coin:
"\<not> ?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n"