# HG changeset patch
# User wenzelm
# Date 955575966 -7200
# Node ID ef6badee7dd6b5c666e1e2415e0c50c6f30b691b
# Parent  734a0206e9f90da4590cb80f59ee1f00f3300b11
improved 'induct(_tac)' syntax;

diff -r 734a0206e9f9 -r ef6badee7dd6 doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Wed Apr 12 23:45:21 2000 +0200
+++ b/doc-src/IsarRef/hol.tex	Wed Apr 12 23:46:06 2000 +0200
@@ -234,11 +234,9 @@
 \begin{rail}
   'cases' ('simplified' ':')? term? rule?  ;
 
-  'induct' ('stripped' ':')? (inst * 'and') rule?
+  'induct' ('stripped' ':')? (insts * 'and') rule?
   ;
 
-  inst: (term +)
-  ;
   rule: ('type' | 'set') ':' nameref | 'rule' ':' thmref
   ;
 \end{rail}
@@ -345,7 +343,7 @@
 \begin{rail}
   casetac goalspec? term rule?
   ;
-  inducttac goalspec? (var +) rule?
+  inducttac goalspec? (insts * 'and') rule?
   ;
 
   rule: ('rule' ':' thmref)
@@ -353,9 +351,10 @@
 \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}