doc-src/TutorialI/fp.tex

 and can be skipped by casual readers.
 
 There are two kinds of commands used during a proof: the actual proof
 commands and auxiliary commands for examining the proof state and controlling
 the display. Simple proof commands are of the form
-\isacommand{apply}\isa{(method)}\indexbold{apply} where \bfindex{method} is a
-synonym for ``theorem proving function''. Typical examples are
-\isa{induct_tac} and \isa{auto}. Further methods are introduced throughout
-the tutorial.  Unless stated otherwise you may assume that a method attacks
-merely the first subgoal. An exception is \isa{auto} which tries to solve all
-subgoals.
-
-The most useful auxiliary commands are:
+\commdx{apply}\isa{(method)}, where \isa{method} is typically 
+\isa{induct_tac} or \isa{auto}.  All such theorem proving operations
+are referred to as \bfindex{methods}, and further ones are
+introduced throughout the tutorial.  Unless stated otherwise, you may
+assume that a method attacks merely the first subgoal. An exception is
+\isa{auto}, which tries to solve all subgoals.
+
+The most useful auxiliary commands are as follows:
 \begin{description}
-\item[Undoing:] \isacommand{undo}\indexbold{*undo} undoes the effect of the
+\item[Undoing:] \commdx{undo} undoes the effect of
+the
   last command; \isacommand{undo} can be undone by
-  \isacommand{redo}\indexbold{*redo}.  Both are only needed at the shell
+  \commdx{redo}.  Both are only needed at the shell
   level and should not occur in the final theory.
-\item[Printing the current state:] \isacommand{pr}\indexbold{*pr} redisplays
+\item[Printing the current state:] \commdx{pr}
+redisplays
   the current proof state, for example when it has scrolled past the top of
   the screen.
 \item[Limiting the number of subgoals:] \isacommand{pr}~$n$ tells Isabelle to
   print only the first $n$ subgoals from now on and redisplays the current
   proof state. This is helpful when there are many subgoals.
 \item[Modifying the order of subgoals:]
-\isacommand{defer}\indexbold{*defer} moves the first subgoal to the end and
-\isacommand{prefer}\indexbold{*prefer}~$n$ moves subgoal $n$ to the front.
+\commdx{defer} moves the first subgoal to the end and
+\commdx{prefer}~$n$ moves subgoal $n$ to the front.
 \item[Printing theorems:]
-  \isacommand{thm}\indexbold{*thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
+  \commdx{thm}~\textit{name}$@1$~\dots~\textit{name}$@n$
   prints the named theorems.
 \item[Displaying types:] We have already mentioned the flag
   \ttindex{show_types} above. It can also be useful for detecting typos in
   formulae early on. For example, if \texttt{show_types} is set and the goal
   \isa{rev(rev xs) = xs} is started, Isabelle prints the additional output

 ~~re~::~'a~list~{\isasymRightarrow}~'a~list\isanewline
 ~~xs~::~'a~list%
 \end{isabelle}%
 \par\noindent
 would have alerted us because of the unexpected variable \isa{re}.
-\item[Reading terms and types:] \isacommand{term}\indexbold{*term}
+\item[Reading terms and types:] \commdx{term}
   \textit{string} reads, type-checks and prints the given string as a term in
   the current context; the inferred type is output as well.
-  \isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given
+  \commdx{typ} \textit{string} reads and prints the given
   string as a type in the current context.
 \item[(Re)loading theories:] When you start your interaction you must open a
   named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle
   automatically loads all the required parent theories from their respective
   files (which may take a moment, unless the theories are already loaded and
   the files have not been modified).
   
   If you suddenly discover that you need to modify a parent theory of your
   current theory, you must first abandon your current theory\indexbold{abandon
   theory}\indexbold{theory!abandon} (at the shell
-  level type \isacommand{kill}\indexbold{*kill}). After the parent theory has
+  level type \commdx{kill}). After the parent theory has
   been modified, you go back to your original theory. When its first line
   \isa{\isacommand{theory}~T~=~\dots~:} is processed, the
   modified parent is reloaded automatically.
   
 %  The only time when you need to load a theory by hand is when you simply
 %  want to check if it loads successfully without wanting to make use of the
 %  theory itself. This you can do by typing
-%  \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
+%  \isa{\commdx{use\_thy}~"T"}.
 \end{description}
 Further commands are found in the Isabelle/Isar Reference Manual.
 
 We now examine Isabelle's functional programming constructs systematically,
 starting with inductive datatypes.

 Lists are one of the essential datatypes in computing. Readers of this
 tutorial and users of HOL need to be familiar with their basic operations.
 Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
 \isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
 The latter contains many further operations. For example, the functions
-\isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first
+\cdx{hd} (``head'') and \cdx{tl} (``tail'') return the first
 element and the remainder of a list. (However, pattern-matching is usually
 preferable to \isa{hd} and \isa{tl}.)  
 Also available are higher-order functions like \isa{map} and \isa{filter}.
 Theory \isa{List} also contains
 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates

 primitive recursive function definitions.
 
 Every datatype $t$ comes equipped with a \isa{size} function from $t$ into
 the natural numbers (see~{\S}\ref{sec:nat} below). For lists, \isa{size} is
 just the length, i.e.\ \isa{size [] = 0} and \isa{size(x \# xs) = size xs +
-  1}.  In general, \isaindexbold{size} returns \isa{0} for all constructors
+  1}.  In general, \cdx{size} returns \isa{0} for all constructors
 that do not have an argument of type $t$, and for all other constructors
 \isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because
 \isa{size} is defined on every datatype, it is overloaded; on lists
-\isa{size} is also called \isaindexbold{length}, which is not overloaded.
+\isa{size} is also called \sdx{length}, which is not overloaded.
 Isabelle will always show \isa{size} on lists as \isa{length}.
 
 
 \subsection{Primitive Recursion}