--- 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