src/HOL/Library/While_Combinator.thy

  An example of using the @{term while} combinator.\footnote{It is safe
  to keep the example here, since there is no effect on the current
  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
     apply (simp add: aux set_eq_subset)
     txt {* The fixpoint computation is performed purely by rewriting: *}