doc-src/IsarRef/hol.tex

 about large specifications.
 
 \begin{rail}
   'cases' ('simplified' ':')? term? rule?  ;
 
-  'induct' ('stripped' ':')? (inst * 'and') rule?
-  ;
-
-  inst: (term +)
-  ;
+  'induct' ('stripped' ':')? (insts * 'and') rule?
+  ;
+
   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
   ;
 \end{rail}
 
 \begin{descr}

 \railterm{inducttac}
 
 \begin{rail}
   casetac goalspec? term rule?
   ;
-  inducttac goalspec? (var +) rule?
+  inducttac goalspec? (insts * 'and') rule?
   ;
 
   rule: ('rule' ':' thmref)
   ;
 \end{rail}
 
 By default, $case_tac$ and $induct_tac$ admit to reason about datatypes only,
-unless an alternative explicit rule is given.  Also note that named local
-contexts (see \S\ref{sec:cases}) are not provided as would be by the proper
-$induct$ and $cases$ proof methods (see \S\ref{sec:induct-method-proper}).
+unless an alternative explicit rule is given; only variables may be given as
+instantiation for $induct_tac$.  Also note that named local contexts (see
+\S\ref{sec:cases}) are not provided as would be by the proper $induct$ and
+$cases$ proof methods (see \S\ref{sec:induct-method-proper}).
 
 
 \section{Arithmetic}
 
 \indexisarmeth{arith}