--- a/doc-src/TutorialI/Sets/sets.tex Wed Jul 11 17:55:46 2001 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex Thu Jul 12 16:33:36 2001 +0200
@@ -1017,8 +1017,8 @@
operators only in \S\ref{sec:VMC}.
\end{warn}
-The theory applies only to monotonic functions. Isabelle's
-definition of monotone is overloaded over all orderings:
+The theory applies only to monotonic functions.\index{monotone functions|bold}
+Isabelle's definition of monotone is overloaded over all orderings:
\begin{isabelle}
mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%
\rulename{mono_def}