# HG changeset patch
# User nipkow
# Date 1391532255 -3600
# Node ID 908fd015cf2e5b6145ba11b39fdb10ac481e817e
# Parent  834a84553e0289d6d74b13b7ae9e47dccea3ac6b
tuned

diff -r 834a84553e02 -r 908fd015cf2e src/Doc/ProgProve/Bool_nat_list.thy
--- 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}
 
diff -r 834a84553e02 -r 908fd015cf2e src/Doc/ProgProve/Types_and_funs.thy
--- 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"}.