diff -r a39e5d43de55 -r bbefb6ce5cb2 doc-src/TutorialI/Recdef/Induction.thy
--- a/doc-src/TutorialI/Recdef/Induction.thy	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Induction.thy	Fri Sep 01 19:09:44 2000 +0200
@@ -10,7 +10,7 @@
 again induction. But this time the structural form of induction that comes
 with datatypes is unlikely to work well---otherwise we could have defined the
 function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
-proves a suitable induction rule $f$\isa{.induct} that follows the
+proves a suitable induction rule $f$@{text".induct"} that follows the
 recursion pattern of the particular function $f$. We call this
 \textbf{recursion induction}. Roughly speaking, it
 requires you to prove for each \isacommand{recdef} equation that the property
@@ -21,16 +21,16 @@
 lemma "map f (sep(x,xs)) = sep(f x, map f xs)";
 
 txt{*\noindent
-involving the predefined \isa{map} functional on lists: \isa{map f xs}
-is the result of applying \isa{f} to all elements of \isa{xs}. We prove
-this lemma by recursion induction w.r.t. \isa{sep}:
+involving the predefined @{term"map"} functional on lists: @{term"map f xs"}
+is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove
+this lemma by recursion induction w.r.t. @{term"sep"}:
 *}
 
 apply(induct_tac x xs rule: sep.induct);
 
 txt{*\noindent
 The resulting proof state has three subgoals corresponding to the three
-clauses for \isa{sep}:
+clauses for @{term"sep"}:
 \begin{isabelle}
 ~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
 ~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
@@ -47,24 +47,24 @@
 Try proving the above lemma by structural induction, and you find that you
 need an additional case distinction. What is worse, the names of variables
 are invented by Isabelle and have nothing to do with the names in the
-definition of \isa{sep}.
+definition of @{term"sep"}.
 
 In general, the format of invoking recursion induction is
-\begin{ttbox}
-apply(induct_tac \(x@1 \dots x@n\) rule: \(f\).induct)
-\end{ttbox}\index{*induct_tac}%
+\begin{quote}
+\isacommand{apply}@{text"(induct_tac ("}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"}
+\end{quote}\index{*induct_tac}%
 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
 name of a function that takes an $n$-tuple. Usually the subgoal will
 contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
-induction rules do not mention $f$ at all. For example \isa{sep.induct}
+induction rules do not mention $f$ at all. For example @{thm[source]sep.induct}
 \begin{isabelle}
 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
 ~~{\isasymAnd}a~x.~P~a~[x];\isanewline
 ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
 {\isasymLongrightarrow}~P~u~v%
 \end{isabelle}
-merely says that in order to prove a property \isa{P} of \isa{u} and
-\isa{v} you need to prove it for the three cases where \isa{v} is the
+merely says that in order to prove a property @{term"P"} of @{term"u"} and
+@{term"v"} you need to prove it for the three cases where @{term"v"} is the
 empty list, the singleton list, and the list with at least two elements
 (in which case you may assume it holds for the tail of that list).
 *}