--- a/src/Coinductive.v	Fri Dec 16 13:28:11 2011 -0500
+++ b/src/Coinductive.v	Fri Mar 02 09:58:00 2012 -0500
@@ -638,19 +638,3 @@
 (* end thide *)
 
 (** In this form, the theorem tells us that the optimizer preserves observable behavior of both terminating and nonterminating programs, but we did not have to do more work than for the case of terminating programs alone.  We merely took the natural inductive definition for terminating executions, made it co-inductive, and applied the appropriate co-induction principle.  Curious readers might experiment with adding command constructs like %\texttt{%#<tt>#if#</tt>#%}%; the same proof should continue working, after the co-induction principle is extended to the new evaluation rules. *)
-
-
-(** * Exercises *)
-
-(** %\begin{enumerate}%#<ol>#
-
-%\item%#<li># %\begin{enumerate}%#<ol>#
-  %\item%#<li># Define a co-inductive type of infinite trees carrying data of a fixed parameter type.  Each node should contain a data value and two child trees.#</li>#
-  %\item%#<li># Define a function [everywhere] for building a tree with the same data value at every node.#</li>#
-  %\item%#<li># Define a function [map] for building an output tree out of two input trees by traversing them in parallel and applying a two-argument function to their corresponding data values.#</li>#
-  %\item%#<li># Define a tree [falses] where every node has the value [false].#</li>#
-  %\item%#<li># Define a tree [true_false] where the root node has value [true], its children have value [false], all nodes at the next have the value [true], and so on, alternating boolean values from level to level.#</li>#
-  %\item%#<li># Prove that [true_false] is equal to the result of mapping the boolean %``%#"#or#"#%''% function [orb] over [true_false] and [falses].  You can make [orb] available with [Require Import Bool.].  You may find the lemma [orb_false_r] from the same module helpful.  Your proof here should not be about the standard equality [=], but rather about some new equality relation that you define.#</li>#
-#</ol>#%\end{enumerate}% #</li>#
-
-#</ol>#%\end{enumerate}% *)