diff -r 7ffcd6f2890d -r b11d73dbfb76 src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Mon Jul 29 18:06:39 2013 +0200
+++ b/src/Doc/ProgProve/Logic.thy	Mon Jul 29 22:17:19 2013 +0200
@@ -477,10 +477,10 @@
 
 Inductive definitions are the third important definition facility, after
 datatypes and recursive function.
-\sem
+\ifsem
 In fact, they are the key construct in the
 definition of operational semantics in the second part of the book.
-\endsem
+\fi
 
 \subsection{An Example: Even Numbers}
 \label{sec:Logic:even}
@@ -670,10 +670,10 @@
 Evenness is really more conveniently expressed recursively than inductively.
 As a second and very typical example of an inductive definition we define the
 reflexive transitive closure.
-\sem
+\ifsem
 It will also be an important building block for
 some of the semantics considered in the second part of the book.
-\endsem
+\fi
 
 The reflexive transitive closure, called @{text star} below, is a function
 that maps a binary predicate to another binary predicate: if @{text r} is of