304       done

   304       done

   305   qed

   305   qed

   306 qed

   306 qed

   307 

   307 

   308 text {*

   308 text {*

   309   The point of these examples is to get a feeling what the automatic proofs 

   311   The point of these examples is to get a feeling what the automatic proofs 

   310   should do in order to solve all inductive definitions we throw at them. For this 

   312   should do in order to solve all inductive definitions we throw at them. For this 

   311   it is instructive to look at the general construction principle 

   313   it is instructive to look at the general construction principle 

   312   of inductive definitions, which we shall do in the next section.

   314   of inductive definitions, which we shall do in the next section.

   313 *}

   315 *}