--- a/doc-src/TutorialI/basics.tex Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/basics.tex Fri Sep 01 19:09:44 2000 +0200
@@ -71,7 +71,7 @@
proofs are in separate ML files.
\begin{warn}
- HOL contains a theory \ttindexbold{Main}, the union of all the basic
+ HOL contains a theory \isaindexbold{Main}, the union of all the basic
predefined theories like arithmetic, lists, sets, etc.\ (see the online
library). Unless you know what you are doing, always include \texttt{Main}
as a direct or indirect parent theory of all your theories.
@@ -115,7 +115,7 @@
called \bfindex{type inference}) and keeps quiet about it. Occasionally
this may lead to misunderstandings between you and the system. If anything
strange happens, we recommend to set the \rmindex{flag}
- \ttindexbold{show_types} that tells Isabelle to display type information
+ \isaindexbold{show_types} that tells Isabelle to display type information
that is usually suppressed: simply type
\begin{ttbox}
ML "set show_types"
@@ -198,7 +198,7 @@
input, you can see which parentheses are dropped---they were superfluous. If
you are unsure how to interpret Isabelle's output because you don't know
where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag}
-\ttindexbold{show_brackets}:
+\isaindexbold{show_brackets}:
\begin{ttbox}
ML "set show_brackets"; \(\dots\); ML "reset show_brackets";
\end{ttbox}