--- a/doc-src/TutorialI/Types/numerics.tex Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Types/numerics.tex Tue Jul 17 13:46:21 2001 +0200
@@ -76,7 +76,7 @@
\end{warn}
\begin{warn}
-\index{recdef@\protect\isacommand{recdef} (command)!and numeric literals}
+\index{recdef@\isacommand {recdef} (command)!and numeric literals}
Numeric literals are not constructors and therefore
must not be used in patterns. For example, this declaration is
rejected:
@@ -434,7 +434,7 @@
Type \isa{real} is only available in the logic HOL-Real, which
is HOL extended with the rather substantial development of the real
numbers. Base your theory upon theory
-\isa{Real}, not the usual \isa{Main}.%
+\thydx{Real}, not the usual \isa{Main}.%
\index{real numbers|)}\index{*real (type)|)}
Launch Isabelle using the command
\begin{verbatim}