--- a/src/HOL/Probability/ex/Dining_Cryptographers.thy Tue Feb 28 20:20:09 2012 +0100
+++ b/src/HOL/Probability/ex/Dining_Cryptographers.thy Tue Feb 28 21:53:36 2012 +0100
@@ -82,7 +82,7 @@
assumes "dc \<in> dining_cryptographers"
shows "result dc \<longleftrightarrow> (payer dc \<noteq> None)"
proof -
- let "?XOR f l" = "foldl (op \<noteq>) False (map f [0..<l])"
+ let ?XOR = "\<lambda>f l. foldl (op \<noteq>) False (map f [0..<l])"
have foldl_coin:
"\<not> ?XOR (\<lambda>c. coin dc c \<noteq> coin dc (c + 1)) n"
@@ -306,8 +306,8 @@
assumes "xs \<in> inversion ` dc_crypto"
shows "card {dc \<in> dc_crypto. inversion dc = xs} = 2 * n"
proof -
- let "?set i" = "{dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}"
- let "?sets" = "{?set i | i. i < n}"
+ let ?set = "\<lambda>i. {dc \<in> dc_crypto. payer dc = Some i \<and> inversion dc = xs}"
+ let ?sets = "{?set i | i. i < n}"
have [simp]: "length xs = n" using assms
by (auto simp: dc_crypto inversion_def_raw)