doc-src/IsarRef/hol.tex

   ;
 \end{rail}
 
 \begin{descr}
 \item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the
-  induction rule of the type/set/function specified by $kind$ and instantiated
-  by $insts$.  The latter either consists of pairs $P$ $x$ (induction
-  predicate and variable), where $P$ is optional.  If $kind$ is omitted, the
-  default is to pick a datatype induction rule according to the type of some
-  induction variable, which may not be omitted that case.
+  induction rule of the type~/ set~/ function specified by $kind$ and
+  instantiated by $insts$.  The latter either consists of pairs $P$ $x$
+  (induction predicate and variable), where $P$ is optional.  If $kind$ is
+  omitted, the default is to pick a datatype induction rule according to the
+  type of some induction variable, which may not be omitted that case.
 \end{descr}
 
 
 \section{Arithmetic}