diff -r 74e970389def -r e14029f92770 src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Mon Jan 29 23:02:21 2001 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Mon Jan 29 23:54:56 2001 +0100
@@ -94,7 +94,7 @@
   "[| P s;
       !!s. [| P s; b s  |] ==> P (c s);
       !!s. [| P s; \<not> b s  |] ==> Q s;
-      wf r; 
+      wf r;
       !!s. [| P s; b s  |] ==> (c s, s) \<in> r |] ==>
    Q (while b c s)"
 apply (rule while_rule_lemma)
@@ -130,25 +130,27 @@
 done
 
 
-(*
 text {*
- An example of using the @{term while} combinator.
+ 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.}
 *}
 
-lemma aux: "{f n | n. A n \<or> B n} = {f n | n. A n} \<union> {f n | n. B n}"
-  apply blast
-  done
-
 theorem "P (lfp (\<lambda>N::int set. {#0} \<union> {(n + #2) mod #6 | n. n \<in> N})) =
     P {#0, #4, #2}"
-  apply (subst lfp_conv_while [where ?U = "{#0, #1, #2, #3, #4, #5}"])
-     apply (rule monoI)
+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
-   apply simp
-  apply (simp add: aux set_eq_subset)
-  txt {* The fixpoint computation is performed purely by rewriting: *}
-  apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
-  done
-*)
+    done
+  show ?thesis
+    apply (subst lfp_conv_while [where ?U = "{#0, #1, #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: *}
+    apply (simp add: while_unfold aux set_eq_subset del: subset_empty)
+    done
+qed
 
 end