1.1 --- a/src/HOL/Library/While_Combinator.thy	Tue Oct 23 22:57:52 2001 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Tue Oct 23 22:58:15 2001 +0200
     1.3 @@ -135,14 +135,13 @@
     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. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = P {0, 4, 2}"
    1.10  proof -
    1.11    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.12      apply blast
    1.13      done
    1.14    show ?thesis
    1.15 -    apply (subst lfp_conv_while [where ?U = "{Numeral0, Numeral1, 2, 3, 4, 5}"])
    1.16 +    apply (subst lfp_conv_while [where ?U = "{0, 1, 2, 3, 4, 5}"])
    1.17         apply (rule monoI)
    1.18        apply blast
    1.19       apply simp