--- a/src/Doc/ProgProve/Bool_nat_list.thy Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Mon Jul 29 22:17:19 2013 +0200
@@ -397,7 +397,8 @@
@{text"\""}@{thm map.simps(1)}@{text"\" |"}\\
@{text"\""}@{thm map.simps(2)}@{text"\""}
\end{isabelle}
-\sem
+
+\ifsem
Also useful are the \concept{head} of a list, its first element,
and the \concept{tail}, the rest of the list:
\begin{isabelle}
@@ -412,7 +413,7 @@
Note that since HOL is a logic of total functions, @{term"hd []"} is defined,
but we do now know what the result is. That is, @{term"hd []"} is not undefined
but underdefined.
-\endsem
+\fi
%
\subsection{Exercises}