1.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Apr 16 12:09:31 2004 +0200
     1.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Apr 16 13:51:04 2004 +0200
     1.3 @@ -141,12 +141,11 @@
     1.4  
     1.5  
     1.6  text {*
     1.7 - An example of using the @{term while} combinator.\footnote{It is safe
     1.8 - to keep the example here, since there is no effect on the current
     1.9 - theory.}
    1.10 + An example of using the @{term while} combinator.
    1.11  *}
    1.12  
    1.13 -theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = P {0, 4, 2}"
    1.14 +theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
    1.15 +  P {0, 4, 2}"
    1.16  proof -
    1.17    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.18      apply blast