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