src/HOL/Library/While_Combinator.thy
 changeset 11704 3c50a2cd6f00 parent 11701 3d51fbf81c17 child 11914 bca734def300
```     1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Oct 05 23:58:52 2001 +0200
1.2 +++ b/src/HOL/Library/While_Combinator.thy	Sat Oct 06 00:02:46 2001 +0200
1.3 @@ -135,14 +135,14 @@
1.4   theory.}
1.5  *}
1.6
1.7 -theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + # 2) mod # 6 | n. n \<in> N})) =
1.8 -    P {Numeral0, # 4, # 2}"
1.9 +theorem "P (lfp (\<lambda>N::int set. {Numeral0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
1.10 +    P {Numeral0, 4, 2}"
1.11  proof -
1.12    have aux: "!!f A B. {f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
1.13      apply blast
1.14      done
1.15    show ?thesis
1.16 -    apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, # 2, # 3, # 4, # 5}"])
1.17 +    apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, 2, 3, 4, 5}"])
1.18         apply (rule monoI)
1.19        apply blast
1.20       apply simp
```