
diff -r 7ffcd6f2890d -r b11d73dbfb76 src/Doc/ProgProve/Bool_nat_list.thy
--- 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}




