src/Doc/ProgProve/Bool_nat_list.thy

 you need to prove
 \begin{enumerate}
 \item the base case @{prop"P(Nil)"} and
 \item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed @{text x} and @{text xs}.
 \end{enumerate}
-This is often called \concept{structural induction}.
+This is often called \concept{structural induction} for lists.
 
 \subsection{The Proof Process}
 
 We will now demonstrate the typical proof process, which involves
 the formulation and proof of auxiliary lemmas.