--- a/src/Doc/ProgProve/Bool_nat_list.thy Tue Feb 04 17:38:54 2014 +0100
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Tue Feb 04 17:44:15 2014 +0100
@@ -226,7 +226,7 @@
\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}
--- a/src/Doc/ProgProve/Types_and_funs.thy Tue Feb 04 17:38:54 2014 +0100
+++ b/src/Doc/ProgProve/Types_and_funs.thy Tue Feb 04 17:44:15 2014 +0100
@@ -39,7 +39,7 @@
\end{tabular}
\end{itemize}
The fact that any value of the datatype is built from the constructors implies
-the structural induction rule: to show
+the \concept{structural induction} rule: to show
$P~x$ for all $x$ of type @{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"},
one needs to show $P(C_i\ x_1 \dots x_{n_i})$ (for each $i$) assuming
$P(x_j)$ for all $j$ where $\tau_{i,j} =$~@{text "('a\<^sub>1,\<dots>,'a\<^sub>n)t"}.