doc-src/IsarRef/Thy/document/intro.tex

 definition foo :: nat where "foo == 1";
 lemma "0 < foo" by (simp add: foo_def);
 end;
 \end{ttbox}
 
-  Note that any Isabelle/Isar command may be retracted by \mbox{\isa{\isacommand{undo}}}.  See the Isabelle/Isar Quick Reference
+  Note that any Isabelle/Isar command may be retracted by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}.  See the Isabelle/Isar Quick Reference
   (\appref{ap:refcard}) for a comprehensive overview of available
   commands and other language elements.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

 
   \end{enumerate}
 
   The Isar proof language is embedded into the new theory format as a
   proper sub-language.  Proof mode is entered by stating some
-  \mbox{\isa{\isacommand{theorem}}} or \mbox{\isa{\isacommand{lemma}}} at the theory level, and
-  left again with the final conclusion (e.g.\ via \mbox{\isa{\isacommand{qed}}}).
+  \hyperlink{command.theorem}{\mbox{\isa{\isacommand{theorem}}}} or \hyperlink{command.lemma}{\mbox{\isa{\isacommand{lemma}}}} at the theory level, and
+  left again with the final conclusion (e.g.\ via \hyperlink{command.qed}{\mbox{\isa{\isacommand{qed}}}}).
   A few theory specification mechanisms also require some proof, such
-  as HOL's \mbox{\isa{\isacommand{typedef}}} which demands non-emptiness of the
+  as HOL's \hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}} which demands non-emptiness of the
   representing sets.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isamarkupsubsection{Document preparation \label{sec:document-prep}%