--- a/src/HOL/Library/While_Combinator.thy Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Library/While_Combinator.thy Sat Oct 06 00:02:46 2001 +0200
@@ -135,14 +135,14 @@
theory.}
*}
-theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + # 2) mod # 6 | n. n \<in> N})) =
- P {Numeral0, # 4, # 2}"
+theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
+ P {Numeral0, 4, 2}"
proof -
have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
apply blast
done
show ?thesis
- apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, # 2, # 3, # 4, # 5}"])
+ apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, 2, 3, 4, 5}"])
apply (rule monoI)
apply blast
apply simp