src/HOL/Library/While_Combinator.thy
changeset 14589 feae7b5fd425
parent 14300 bf8b8c9425c3
child 14706 71590b7733b7
--- a/src/HOL/Library/While_Combinator.thy	Fri Apr 16 12:09:31 2004 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Fri Apr 16 13:51:04 2004 +0200
@@ -141,12 +141,11 @@
 
 
 text {*
- 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.}
+ An example of using the @{term while} combinator.
 *}
 
-theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) = P {0, 4, 2}"
+theorem "P (lfp (\<lambda>N::int set. {0} \<union> {(n + 2) mod 6 | n. n \<in> N})) =
+  P {0, 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